# HG changeset patch # User wenzelm # Date 1512571595 -3600 # Node ID 909dcdec21221f6dd9dbb5c86729c734ba905768 # Parent e77c5bfca9aae297469bb6e815d72da6bf5eb42d more embedded cartouche arguments; more uniform LaTeX output for control symbols; diff -r e77c5bfca9aa -r 909dcdec2122 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Wed Dec 06 14:19:36 2017 +0100 +++ b/lib/texinputs/isabelle.sty Wed Dec 06 15:46:35 2017 +0100 @@ -125,6 +125,9 @@ \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} \newcommand{\isacommand}[1]{\isakeyword{#1}} +\newcommand{\isakeywordcontrol}[1] +{\emph{\bf\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}} + \newcommand{\isamarkupheader}[1]{\section{#1}} \newcommand{\isamarkupchapter}[1]{\chapter{#1}} \newcommand{\isamarkupsection}[1]{\section{#1}} diff -r e77c5bfca9aa -r 909dcdec2122 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Wed Dec 06 14:19:36 2017 +0100 +++ b/lib/texinputs/isabellesym.sty Wed Dec 06 15:46:35 2017 +0100 @@ -367,7 +367,46 @@ \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymcomment}{\isatext{---}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} -\newcommand{\isactrlundefined}{\isakeyword{undefined}\ } -\newcommand{\isactrlfile}{\isakeyword{file}\ } -\newcommand{\isactrldir}{\isakeyword{dir}\ } -\newcommand{\isactrlhere}{\isakeyword{here}\ } + +\newcommand{\isactrlassert}{\isakeywordcontrol{assert}} +\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} +\newcommand{\isactrlclass}{\isakeywordcontrol{class}} +\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} +\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} +\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} +\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} +\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} +\newcommand{\isactrlcontext}{\isakeywordcontrol{context}} +\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} +\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} +\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} +\newcommand{\isactrldir}{\isakeywordcontrol{dir}} +\newcommand{\isactrlfile}{\isakeywordcontrol{file}} +\newcommand{\isactrlhere}{\isakeywordcontrol{here}} +\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} +\newcommand{\isactrllocale}{\isakeywordcontrol{locale}} +\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} +\newcommand{\isactrlmethod}{\isakeywordcontrol{method}} +\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} +\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} +\newcommand{\isactrlpath}{\isakeywordcontrol{path}} +\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} +\newcommand{\isactrlprint}{\isakeywordcontrol{print}} +\newcommand{\isactrlprop}{\isakeywordcontrol{prop}} +\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} +\newcommand{\isactrlsort}{\isakeywordcontrol{sort}} +\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} +\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} +\newcommand{\isactrlterm}{\isakeywordcontrol{term}} +\newcommand{\isactrltheory}{\isakeywordcontrol{theory}} +\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} +\newcommand{\isactrltyp}{\isakeywordcontrol{typ}} +\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} +\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} +\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} +\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} + +\newcommand{\isactrlcode}{\isakeywordcontrol{code}} +\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} +\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} +\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} diff -r e77c5bfca9aa -r 909dcdec2122 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Doc/Implementation/Logic.thy Wed Dec 06 15:46:35 2017 +0100 @@ -171,13 +171,13 @@ \end{matharray} @{rail \ - @@{ML_antiquotation class} name + @@{ML_antiquotation class} embedded ; @@{ML_antiquotation sort} sort ; (@@{ML_antiquotation type_name} | @@{ML_antiquotation type_abbrev} | - @@{ML_antiquotation nonterminal}) name + @@{ML_antiquotation nonterminal}) embedded ; @@{ML_antiquotation typ} type \} @@ -392,7 +392,7 @@ @{rail \ (@@{ML_antiquotation const_name} | - @@{ML_antiquotation const_abbrev}) name + @@{ML_antiquotation const_abbrev}) embedded ; @@{ML_antiquotation const} ('(' (type + ',') ')')? ; diff -r e77c5bfca9aa -r 909dcdec2122 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Doc/Implementation/ML.thy Wed Dec 06 15:46:35 2017 +0100 @@ -695,7 +695,7 @@ @{rail \ @@{ML_antiquotation make_string} ; - @@{ML_antiquotation print} @{syntax name}? + @@{ML_antiquotation print} embedded? \} \<^descr> \@{make_string}\ inlines a function to print arbitrary values similar to diff -r e77c5bfca9aa -r 909dcdec2122 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Doc/Implementation/Prelim.thy Wed Dec 06 15:46:35 2017 +0100 @@ -142,9 +142,9 @@ \end{matharray} @{rail \ - @@{ML_antiquotation theory} name? + @@{ML_antiquotation theory} embedded? ; - @@{ML_antiquotation theory_context} name + @@{ML_antiquotation theory_context} embedded \} \<^descr> \@{theory}\ refers to the background theory of the current context --- as @@ -938,7 +938,7 @@ \end{matharray} @{rail \ - @@{ML_antiquotation binding} name + @@{ML_antiquotation binding} embedded \} \<^descr> \@{binding name}\ produces a binding with base name \name\ and the source diff -r e77c5bfca9aa -r 909dcdec2122 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Dec 06 15:46:35 2017 +0100 @@ -1307,7 +1307,7 @@ (@@{ML_antiquotation class_syntax} | @@{ML_antiquotation type_syntax} | @@{ML_antiquotation const_syntax} | - @@{ML_antiquotation syntax_const}) name + @@{ML_antiquotation syntax_const}) embedded \} \<^descr> @{command parse_translation} etc. declare syntax translation functions to diff -r e77c5bfca9aa -r 909dcdec2122 src/Doc/Isar_Ref/document/showsymbols --- a/src/Doc/Isar_Ref/document/showsymbols Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Doc/Isar_Ref/document/showsymbols Wed Dec 06 15:46:35 2017 +0100 @@ -5,13 +5,8 @@ $eol = "&"; while () { - if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) { - if ($1 eq "isasym") { - print "\\verb,\\<$2>, & {\\isasym$2} $eol\n"; - } - else { - print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n"; - } + if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) { + print "\\verb,\\<$1>, & {\\isasym$1} $eol\n"; if ("$eol" eq "&") { $eol = "\\\\"; } else { diff -r e77c5bfca9aa -r 909dcdec2122 src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Pure/ML/ml_antiquotation.ML Wed Dec 06 15:46:35 2017 +0100 @@ -41,7 +41,7 @@ inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #> value (Binding.make ("binding", \<^here>)) - (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> + (Scan.lift (Parse.position Args.embedded) >> ML_Syntax.make_binding) #> value (Binding.make ("cartouche", \<^here>)) (Scan.lift Args.cartouche_input >> (fn source => diff -r e77c5bfca9aa -r 909dcdec2122 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Wed Dec 06 15:46:35 2017 +0100 @@ -41,7 +41,7 @@ val _ = Theory.setup (ML_Antiquotation.value @{binding system_option} - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => let val markup = Options.default_markup (name, pos) handle ERROR msg => @@ -57,13 +57,13 @@ in ML_Syntax.print_string name end)) #> ML_Antiquotation.value @{binding theory} - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => (Theory.check ctxt (name, pos); "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value @{binding theory_context} - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => (Theory.check ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> @@ -85,7 +85,7 @@ "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.inline @{binding method} - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Method.check_name ctxt (name, pos))))); @@ -93,7 +93,7 @@ val _ = Theory.setup (ML_Antiquotation.inline @{binding locale} - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => Locale.check (Proof_Context.theory_of ctxt) (name, pos) |> ML_Syntax.print_string))); @@ -260,14 +260,14 @@ val _ = Theory.setup (ML_Antiquotation.value @{binding keyword} - (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true))) + (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> ML_Antiquotation.value @{binding command_keyword} - (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) => + (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; diff -r e77c5bfca9aa -r 909dcdec2122 src/Pure/Tools/named_theorems.ML --- a/src/Pure/Tools/named_theorems.ML Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Pure/Tools/named_theorems.ML Wed Dec 06 15:46:35 2017 +0100 @@ -98,7 +98,7 @@ val _ = Theory.setup (ML_Antiquotation.inline @{binding named_theorems} - (Args.context -- Scan.lift (Parse.position Args.name) >> + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name)))); end; diff -r e77c5bfca9aa -r 909dcdec2122 src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Pure/Tools/plugin.ML Wed Dec 06 15:46:35 2017 +0100 @@ -41,7 +41,7 @@ val _ = Theory.setup (ML_Antiquotation.inline @{binding plugin} - (Args.context -- Scan.lift (Parse.position Args.name) + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (ML_Syntax.print_string o uncurry check))); diff -r e77c5bfca9aa -r 909dcdec2122 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Dec 06 14:19:36 2017 +0100 +++ b/src/Pure/simplifier.ML Wed Dec 06 15:46:35 2017 +0100 @@ -113,7 +113,7 @@ val _ = Theory.setup (ML_Antiquotation.value @{binding simproc} - (Args.context -- Scan.lift (Parse.position Args.name) + (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, name) => "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));