diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index 9e5772d..2cc4c55 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -26,7 +26,7 @@ define_shortcut* isadof \ \\isadof\ Protege \ \Prot{\'e}g{\'e}\ (* slanted text in contrast to italics *) -define_macro* slanted_text \ \\textsl{\ \}\ +define_macro* slanted_text \ \\textsl{\ _ \}\ (*>*) diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index db1d713..ca125b1 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -33,8 +33,8 @@ define_shortcut* TeXLive \ \\TeXLive\ text\Note that these setups assume that the associated \<^LaTeX> macros are defined, \<^eg>, in the document prelude. \ -define_macro* index \ \\index{\ \}\ -define_macro* bindex \ \\bindex{\ \}\ +define_macro* index \ \\index{\ _ \}\ +define_macro* bindex \ \\bindex{\ _ \}\ ML\ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index d43998a..ad0ef05 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -429,15 +429,21 @@ ML\ val parse_literal = Parse.alt_string || Parse.cartouche val parse_define_shortcut = (Parse.binding -- ((\<^keyword>\\\ || \<^keyword>\==\) |-- parse_literal)) + --|Parse.underscore -- parse_literal -- (Scan.option (\<^keyword>\(\ |-- Parse.ML_source --|\<^keyword>\)\)) -fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K())); - +fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K())) + |define_macro (X,SOME(src:Input.source)) = + let val _ = () + in + (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K())) + end; val _ = Outer_Syntax.command \<^command_keyword>\define_macro*\ "define LaTeX shortcut" (Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o (fold define_macro))); +Parse.underscore; \ diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 59e3210..535107d 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -481,13 +481,14 @@ define_shortcut* eg \ \\eg\ (* Latin: „exemp subsection\Layout Trimming Commands\ -define_macro* hs \ \\hspace{\ \}\ -define_macro* vs \ \\vspace{\ \}\ +define_macro* hs \ \\hspace{\ _ \}\ +define_macro* vs \ \\vspace{\ _ \}\ + +(* setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (K(K())) \ *) +ML\ Parse.real \ + +setup\ DOF_lib.define_macro \<^binding>\vs2\ "\\vspace{" "}" (fn ctxt => fn src => ()) \ -(* -setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (K(K())) \ -setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (K(K())) \ -*) define_shortcut* clearpage \ \\clearpage{}\