new set of macros : author* and abstract* --- not working yet

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -16,12 +16,24 @@ setup \<open>   DOF_lib.define_shortcut \<^binding>\<open>csp\<close>       "CSP
 
 title*[tit::title]\<open>Philosophers may Dine - Definitively!\<close>
 
-text*[safouan::author, email="''safouan.taha@lri.fr''", affiliation="\<open>LRI, CentraleSupelec\<close>"]
+(* new crashing variant 1:
-     \<open>Safouan Taha\<close>
+author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
+        \<open>Safouan Taha\<close>
+
+*)
+
+(* new crashing variant 2:
+author*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
+        \<open>Safouan Taha\<close>
+
+*)
+text*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
+        \<open>Safouan Taha\<close>
+
 text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
-     \<open>Burkhart Wolff\<close>
+        \<open>Burkhart Wolff\<close>
-text*[lina::author,email="''lina.ye@lri.fr''", affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
+text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
-     \<open>Lina Ye\<close>
+        \<open>Lina Ye\<close>
     
 text*[abs::abstract, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
                                    \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]

src/DOF/Isa_COL.thy

@@ -97,11 +97,11 @@ fun enriched_formal_statement_command ncid (S: (string * string) list) =
    in  gen_enriched_document_command {inline=true} transform_cid transform_attr end;
 
 fun enriched_formal_statement_command0 ncid (S: (string * string) list) =
-   let val transform_cid = case ncid of  NONE => I
+   let fun transform_cid NONE X = X
-                                       | SOME(ncid) => 
+          |transform_cid (SOME ncid) NONE =  (SOME(ncid,@{here}))
-                                            (fn X => case X of NONE => (SOME(ncid,@{here}))
+          |transform_cid (SOME _) (SOME cid) = (SOME cid)  
-                                                             | _ => X)  
+       fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs
-   in  gen_enriched_document_command {inline=true} transform_cid I end;
+   in  gen_enriched_document_command {inline=true} (transform_cid ncid) transform_attr end;
 
 
 fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),

src/DOF/Isa_DOF.thy

@@ -1398,9 +1398,13 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
     (* for the moment naive, i.e. without textual normalization of 
        attribute names and adapted term printing *)
     let val l   = "label = "^ (enclose "{" "}" lab)
+        val _   = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) )
         val cid_long = case cid_opt of
-                                NONE => DOF_core.default_cid
+                                NONE => (case DOF_core.get_object_global lab thy of
+                                           NONE => DOF_core.default_cid
+                                         | SOME X => #cid X)
                               | SOME(cid,_) => DOF_core.parse_cid_global thy cid        
+        val _   = writeln("meta_args_2_string cid_long:"^ cid_long )
         val cid_txt  = "type = " ^ (enclose "{" "}" cid_long);
 
         fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2) 
@@ -1455,18 +1459,12 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
     in
       (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"])) 
 end
-(* the following 2 lines set parser and converter for LaTeX generation of meta-attributes. 
-   Currently of *all* commands, no distinction between text* and text command. 
-   This code depends on a MODIFIED Isabelle2017 version resulting from applying the files
-   under src/patches. 
- *)
-(* REMARK PORT 2018 : transmission of meta-args to LaTeX crude and untested. Can be found in
-   present_token. *)
-
 
 end
 \<close>
-ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of 
+
+
+ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of
        text elements - so text*[m<meta-info>]\<open> ... dfgdfg .... \<close> *)
                  
 val _ = Thy_Output.set_meta_args_parser

src/ontologies/scholarly_paper/DOF-scholarly_paper.sty

@@ -119,6 +119,7 @@
   }
 }
 
+\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={author},#1]{\BODY}}
 \provideisadof{text.scholarly_paper.author}%
 [label=,type=%
 ,scholarly_paper.author.email=%

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -29,7 +29,7 @@ doc_class title =
    short_title :: "string option"  <=  "None"
     
 doc_class subtitle =
-   abbrev ::      "string option"       <=  "None"
+   abbrev ::      "string option"  <=  "None"
    
 (* adding a contribution list and checking that it is cited as well in tech as in conclusion. ? *)