More antiquotations

src/DOF/Isa_COL.thy

@@ -125,14 +125,14 @@ fun heading_command (name, pos) descr level =
   Monitor_Command_Parser.document_command (name, pos) descr
     {markdown = false, body = true} (enriched_text_element_cmd level);
 
-val _ = heading_command ("title*", @{here}) "section heading" NONE;
-val _ = heading_command ("subtitle*", @{here}) "section heading" NONE;
-val _ = heading_command ("chapter*", @{here}) "section heading" (SOME (SOME 0));
-val _ = heading_command ("section*", @{here}) "section heading" (SOME (SOME 1));
-val _ = heading_command ("subsection*", @{here}) "subsection heading" (SOME (SOME 2));
-val _ = heading_command ("subsubsection*", @{here}) "subsubsection heading" (SOME (SOME 3));
-val _ = heading_command ("paragraph*", @{here}) "paragraph heading" (SOME (SOME 4));
-val _ = heading_command ("subparagraph*", @{here}) "subparagraph heading" (SOME (SOME 5));
+val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
+val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;
+val _ = heading_command \<^command_keyword>\<open>chapter*\<close> "section heading" (SOME (SOME 0));
+val _ = heading_command \<^command_keyword>\<open>section*\<close> "section heading" (SOME (SOME 1));
+val _ = heading_command \<^command_keyword>\<open>subsection*\<close> "subsection heading" (SOME (SOME 2));
+val _ = heading_command \<^command_keyword>\<open>subsubsection*\<close> "subsubsection heading" (SOME (SOME 3));
+val _ = heading_command \<^command_keyword>\<open>paragraph*\<close> "paragraph heading" (SOME (SOME 4));
+val _ = heading_command \<^command_keyword>\<open>subparagraph*\<close> "subparagraph heading" (SOME (SOME 5));
 
 end 
 end
@@ -238,8 +238,8 @@ ML\<open>
 (* Ontological Macro Command Support                                       *)
 (* *********************************************************************** *)
 
-val _ = Onto_Macros.heading_command ("figure*", @{here}) "figure" NONE;
-val _ = Onto_Macros.heading_command ("side_by_side_figure*", @{here}) "multiple figures" NONE;
+val _ = Onto_Macros.heading_command \<^command_keyword>\<open>figure*\<close> "figure" NONE;
+val _ = Onto_Macros.heading_command \<^command_keyword>\<open>side_by_side_figure*\<close> "multiple figures" NONE;
 \<close>
 
 (*<*)

src/DOF/Isa_DOF.thy

@@ -158,7 +158,7 @@ struct
 
    fun  merge_docclass_tab (otab,otab') = Symtab.merge (op =) (otab,otab') 
 
-   val tag_attr = (Binding.make("tag_attribute",@{here}), \<^Type>\<open>int\<close>, Mixfix.NoSyn)
+   val tag_attr = (\<^binding>\<open>tag_attribute\<close>, \<^Type>\<open>int\<close>, Mixfix.NoSyn)
         (* Attribute hidden to the user and used internally by isabelle_DOF.
            For example, this allows to add a specific id to a class
            to be able to reference the class internally.
@@ -2045,37 +2045,37 @@ fun document_command (name, pos) descr mark cmd =
 (* Core Command Definitions *)
 
 val _ =
-  Outer_Syntax.command @{command_keyword "open_monitor*"} 
+  Outer_Syntax.command \<^command_keyword>\<open>open_monitor*\<close>
                        "open a document reference monitor"
                        (ODL_Meta_Args_Parser.attributes
                         >> (Toplevel.theory o open_monitor_command));
 
 val _ =
-  Outer_Syntax.command @{command_keyword "close_monitor*"} 
+  Outer_Syntax.command \<^command_keyword>\<open>close_monitor*\<close>
                        "close a document reference monitor"
                        (ODL_Meta_Args_Parser.attributes_upd
                         >> (Toplevel.theory o close_monitor_command)); 
 
 
 val _ =
-  Outer_Syntax.command @{command_keyword "update_instance*"} 
+  Outer_Syntax.command \<^command_keyword>\<open>update_instance*\<close>
                        "update meta-attributes of an instance of a document class"
                         (ODL_Meta_Args_Parser.attributes_upd
                          >> (Toplevel.theory o update_instance_command)); 
 
 val _ =
-  document_command ("text*", @{here}) "formal comment (primary style)"
+  document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
     {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I);
 
 
 (* This is just a stub at present *)
 val _ =
-  document_command ("text-macro*", @{here}) "formal comment macro"
+  document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
     {markdown = true, body = true}
     (gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
 
 val _ =
-  Outer_Syntax.command @{command_keyword "declare_reference*"} 
+  Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
                        "declare document reference"
                        (ODL_Meta_Args_Parser.attributes >> (fn (((oid,pos),cid),doc_attrs) =>  
                                       (Toplevel.theory (DOF_core.declare_object_global oid))));
@@ -2523,7 +2523,7 @@ fun read_fields raw_fields ctxt =
       val ctxt' = fold Variable.declare_typ Ts ctxt;
     in (fields, terms, ctxt') end;
 
-val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \<times> string) list",Mixfix.NoSyn),
+val trace_attr = ((\<^binding>\<open>trace\<close>, "(doc_class rexp \<times> string) list",Mixfix.NoSyn),
                   SOME "[]"): ((binding * string * mixfix) * string option)
 
 fun def_cmd (decl, spec, prems, params) lthy =

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -46,12 +46,12 @@ doc_class abstract =
 
 ML\<open>
 val _ =
-  Monitor_Command_Parser.document_command ("abstract*", @{here}) "Textual Definition"
+  Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
     {markdown = true, body = true}
     (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []);
 
 val _ =
-  Monitor_Command_Parser.document_command ("author*", @{here}) "Textual Definition"
+  Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
     {markdown = true, body = true}
     (Onto_Macros.enriched_document_cmd_exp (SOME "author") []);
 \<close>
@@ -289,7 +289,7 @@ setup\<open>Theorem_default_class_setup\<close>
 ML\<open> local open ODL_Meta_Args_Parser in
 
 val _ = 
-  Monitor_Command_Parser.document_command ("Definition*", @{here}) "Textual Definition"
+  Monitor_Command_Parser.document_command \<^command_keyword>\<open>Definition*\<close> "Textual Definition"
     {markdown = true, body = true}
     (fn meta_args => fn thy =>
       let
@@ -301,7 +301,7 @@ val _ =
       end);
 
 val _ =
-  Monitor_Command_Parser.document_command ("Lemma*", @{here}) "Textual Lemma Outline"
+  Monitor_Command_Parser.document_command \<^command_keyword>\<open>Lemma*\<close> "Textual Lemma Outline"
     {markdown = true, body = true}
     (fn meta_args => fn thy =>
       let
@@ -313,7 +313,7 @@ val _ =
       end);
 
 val _ =
-  Monitor_Command_Parser.document_command ("Theorem*", @{here}) "Textual Theorem Outline"
+  Monitor_Command_Parser.document_command \<^command_keyword>\<open>Theorem*\<close> "Textual Theorem Outline"
     {markdown = true, body = true}
     (fn meta_args => fn thy =>
       let