verusdoc: add return names

verus-lang · Oct 24, 2024 · f31d552 · f31d552
1 parent 91cb303
commit f31d552
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 18 deletions.
diff --git a/source/builtin_macros/src/rustdoc.rs b/source/builtin_macros/src/rustdoc.rs
@@ -35,8 +35,8 @@ use syn_verus::punctuated::Punctuated;
 use syn_verus::spanned::Spanned;
 use syn_verus::token;
 use syn_verus::{
-    AttrStyle, Attribute, Block, Expr, ExprBlock, FnMode, Ident, ImplItemMethod, ItemFn, Path,
-    PathArguments, PathSegment, Publish, ReturnType, Signature, TraitItemMethod,
+    AttrStyle, Attribute, Block, Expr, ExprBlock, FnMode, Ident, ImplItemMethod, ItemFn, Pat,
+    PatIdent, Path, PathArguments, PathSegment, Publish, ReturnType, Signature, TraitItemMethod,
 };
 
 /// Check if VERUSDOC=1.
@@ -187,14 +187,20 @@ fn module_path_to_string(p: &Path) -> String {
 
 fn encoded_sig_info(sig: &Signature) -> String {
     let fn_mode = fn_mode_to_string(&sig.mode, &sig.publish);
-    let ret_mode = match &sig.output {
-        ReturnType::Default => "Default",
-        ReturnType::Type(_, tracked_token, _, _) => {
-            if tracked_token.is_some() {
-                "Tracked"
-            } else {
-                "Default"
-            }
+    let (ret_mode, ret_name) = match &sig.output {
+        ReturnType::Default => ("Default", "".to_string()),
+        ReturnType::Type(_, tracked_token, opt_name, _) => {
+            let mode = if tracked_token.is_some() { "Tracked" } else { "Default" };
+
+            let name = match opt_name {
+                None => "".to_string(),
+                Some(b) => match &b.1 {
+                    Pat::Ident(PatIdent { ident, .. }) => ident.to_string(),
+                    _ => "".to_string(),
+                },
+            };
+
+            (mode, name)
         }
     };
 
@@ -215,7 +221,7 @@ fn encoded_sig_info(sig: &Signature) -> String {
     // complicate the post-processing.
 
     let info = format!(
-        r#"// {{ "fn_mode": "{fn_mode:}", "ret_mode": "{ret_mode:}", "param_modes": [{param_modes:}], "broadcast": {broadcast:} }}"#
+        r#"// {{ "fn_mode": "{fn_mode:}", "ret_mode": "{ret_mode:}", "param_modes": [{param_modes:}], "broadcast": {broadcast:}, "ret_name": "{ret_name:}" }}"#
     );
 
     encoded_str("modes", &info)

diff --git a/source/verusdoc/src/main.rs b/source/verusdoc/src/main.rs
@@ -20,6 +20,7 @@ pub enum ParamMode {
 pub struct DocSigInfo {
     pub fn_mode: String,
     pub ret_mode: ParamMode,
+    pub ret_name: String,
     pub param_modes: Vec<ParamMode>,
     pub broadcast: bool,
 }
@@ -209,6 +210,19 @@ fn mk_sig_keyword_node(spec_name: &str) -> NodeRef {
     nr
 }
 
+/// <span class="verus-ret-name">{spec name}</span>
+
+fn mk_ret_name_node(spec_name: &str) -> NodeRef {
+    let t = NodeRef::new_text(spec_name);
+
+    let qual_name = QualName::new(None, ns!(html), local_name!("span"));
+    let nr = NodeRef::new_element(qual_name, vec![]);
+    set_class_attribute(&nr, "verus-ret-name");
+    nr.append(t);
+
+    nr
+}
+
 /// <div class="verus-spec"></div>
 
 fn mk_spec_node() -> NodeRef {
@@ -329,7 +343,7 @@ fn update_sig_info(docblock_elem: &NodeRef, info: UpdateSigMode<'_>) {
 
     let full_text = summary.text_contents();
 
-    let mut splices: Vec<(usize, String)> = vec![];
+    let mut splices: Vec<(usize, String, bool)> = vec![];
 
     let fn_idx = if let Some(fn_idx) = full_text.find("fn") {
         fn_idx
@@ -342,7 +356,7 @@ fn update_sig_info(docblock_elem: &NodeRef, info: UpdateSigMode<'_>) {
             // TODO: separate these if possible
             let broadcast = if info.broadcast { "broadcast ".to_owned() } else { "".to_owned() };
             let fn_mode = format!("{:} ", info.fn_mode);
-            splices.push((fn_idx, broadcast + &fn_mode));
+            splices.push((fn_idx, broadcast + &fn_mode, true));
 
             let arg0_idx = get_arg0_idx(&full_text, fn_idx);
 
@@ -352,7 +366,7 @@ fn update_sig_info(docblock_elem: &NodeRef, info: UpdateSigMode<'_>) {
                 match info.param_modes[i] {
                     ParamMode::Default => {}
                     ParamMode::Tracked => {
-                        splices.push((arg_idx, "tracked ".to_string()));
+                        splices.push((arg_idx, "tracked ".to_string(), true));
                     }
                 }
 
@@ -367,19 +381,26 @@ fn update_sig_info(docblock_elem: &NodeRef, info: UpdateSigMode<'_>) {
                 ParamMode::Tracked => {
                     let arrow_idx = full_text[arg_idx..].find("->").unwrap() + arg_idx;
                     let type_idx = arrow_idx + 3;
-                    splices.push((type_idx, "tracked ".to_string()));
+                    splices.push((type_idx, "tracked ".to_string(), true));
                 }
+            };
+
+            if info.ret_name.len() > 0 {
+                let string_to_insert = format!("{:} : ", info.ret_name);
+                let arrow_idx = full_text[arg_idx..].find("->").unwrap() + arg_idx;
+                let type_idx = arrow_idx + 3;
+                splices.push((type_idx, string_to_insert, false));
             }
         }
         UpdateSigMode::BroadcastGroup => {
-            splices.push((fn_idx, "broadcast group ".to_owned()));
+            splices.push((fn_idx, "broadcast group ".to_owned(), true));
         }
     }
 
     // Reverse order since inserting text should invalidate later indices
-    for (idx, s) in splices.into_iter().rev() {
+    for (idx, s, is_kw) in splices.into_iter().rev() {
         let mut idx = idx;
-        let new_node = mk_sig_keyword_node(&s);
+        let new_node = if is_kw { mk_sig_keyword_node(&s) } else { mk_ret_name_node(&s) };
         do_text_splice(&summary, &new_node, &mut idx, true);
     }
 }