diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 64b5d21..cb354f0 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -16,12 +16,24 @@ setup \ DOF_lib.define_shortcut \<^binding>\csp\ "CSP title*[tit::title]\Philosophers may Dine - Definitively!\ -text*[safouan::author, email="''safouan.taha@lri.fr''", affiliation="\LRI, CentraleSupelec\"] - \Safouan Taha\ +(* new crashing variant 1: +author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] + \Safouan Taha\ + +*) + +(* new crashing variant 2: +author*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] + \Safouan Taha\ + +*) +text*[safouan::author, email="''safouan.taha@lri.fr''",affiliation="\LRI, CentraleSupelec\"] + \Safouan Taha\ + text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\LRI, Université Paris-Saclay\"] - \Burkhart Wolff\ -text*[lina::author,email="''lina.ye@lri.fr''", affiliation="\LRI, Inria, LSV, CentraleSupelec\"] - \Lina Ye\ + \Burkhart Wolff\ +text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\LRI, Inria, LSV, CentraleSupelec\"] + \Lina Ye\ text*[abs::abstract, keywordlist="[\Shallow Embedding\,\Process-Algebra\, \Concurrency\,\Computational Models\]"] diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index ed655c3..40f1181 100755 --- a/src/DOF/Isa_COL.thy +++ b/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 - | SOME(ncid) => - (fn X => case X of NONE => (SOME(ncid,@{here})) - | _ => X) - in gen_enriched_document_command {inline=true} transform_cid I end; + let fun transform_cid NONE X = X + |transform_cid (SOME ncid) NONE = (SOME(ncid,@{here})) + |transform_cid (SOME _) (SOME cid) = (SOME cid) + fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs + 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), diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 68a4bd3..ee14601 100755 --- a/src/DOF/Isa_DOF.thy +++ b/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 \ char list \ 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 \ -ML\ (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of + + +ML\ (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of text elements - so text*[m]\ ... dfgdfg .... \ *) val _ = Thy_Output.set_meta_args_parser diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index 6021704..02bfb6a 100755 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/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=% diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 06f8433..1357c62 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/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. ? *)