more embedded cartouche arguments;
authorwenzelm
Wed Dec 06 15:46:35 2017 +0100 (12 months ago)
changeset 67146909dcdec2122
parent 67145 e77c5bfca9aa
child 67147 dea94b1aabc3
more embedded cartouche arguments;
more uniform LaTeX output for control symbols;
lib/texinputs/isabelle.sty
lib/texinputs/isabellesym.sty
src/Doc/Implementation/Logic.thy
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Prelim.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/document/showsymbols
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/plugin.ML
src/Pure/simplifier.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -125,6 +125,9 @@
     1.4  \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
     1.5  \newcommand{\isacommand}[1]{\isakeyword{#1}}
     1.6  
     1.7 +\newcommand{\isakeywordcontrol}[1]
     1.8 +{\emph{\bf\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
     1.9 +
    1.10  \newcommand{\isamarkupheader}[1]{\section{#1}}
    1.11  \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
    1.12  \newcommand{\isamarkupsection}[1]{\section{#1}}
     2.1 --- a/lib/texinputs/isabellesym.sty	Wed Dec 06 14:19:36 2017 +0100
     2.2 +++ b/lib/texinputs/isabellesym.sty	Wed Dec 06 15:46:35 2017 +0100
     2.3 @@ -367,7 +367,46 @@
     2.4  \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
     2.5  \newcommand{\isasymcomment}{\isatext{---}}
     2.6  \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
     2.7 -\newcommand{\isactrlundefined}{\isakeyword{undefined}\ }
     2.8 -\newcommand{\isactrlfile}{\isakeyword{file}\ }
     2.9 -\newcommand{\isactrldir}{\isakeyword{dir}\ }
    2.10 -\newcommand{\isactrlhere}{\isakeyword{here}\ }
    2.11 +
    2.12 +\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
    2.13 +\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
    2.14 +\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
    2.15 +\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
    2.16 +\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
    2.17 +\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
    2.18 +\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
    2.19 +\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
    2.20 +\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
    2.21 +\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
    2.22 +\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
    2.23 +\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
    2.24 +\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
    2.25 +\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
    2.26 +\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
    2.27 +\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
    2.28 +\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
    2.29 +\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
    2.30 +\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
    2.31 +\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
    2.32 +\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
    2.33 +\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
    2.34 +\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
    2.35 +\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
    2.36 +\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
    2.37 +\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
    2.38 +\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
    2.39 +\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
    2.40 +\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
    2.41 +\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
    2.42 +\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
    2.43 +\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
    2.44 +\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
    2.45 +\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
    2.46 +\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
    2.47 +\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
    2.48 +\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
    2.49 +
    2.50 +\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
    2.51 +\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
    2.52 +\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
    2.53 +\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
     3.1 --- a/src/Doc/Implementation/Logic.thy	Wed Dec 06 14:19:36 2017 +0100
     3.2 +++ b/src/Doc/Implementation/Logic.thy	Wed Dec 06 15:46:35 2017 +0100
     3.3 @@ -171,13 +171,13 @@
     3.4    \end{matharray}
     3.5  
     3.6    @{rail \<open>
     3.7 -  @@{ML_antiquotation class} name
     3.8 +  @@{ML_antiquotation class} embedded
     3.9    ;
    3.10    @@{ML_antiquotation sort} sort
    3.11    ;
    3.12    (@@{ML_antiquotation type_name} |
    3.13     @@{ML_antiquotation type_abbrev} |
    3.14 -   @@{ML_antiquotation nonterminal}) name
    3.15 +   @@{ML_antiquotation nonterminal}) embedded
    3.16    ;
    3.17    @@{ML_antiquotation typ} type
    3.18    \<close>}
    3.19 @@ -392,7 +392,7 @@
    3.20  
    3.21    @{rail \<open>
    3.22    (@@{ML_antiquotation const_name} |
    3.23 -   @@{ML_antiquotation const_abbrev}) name
    3.24 +   @@{ML_antiquotation const_abbrev}) embedded
    3.25    ;
    3.26    @@{ML_antiquotation const} ('(' (type + ',') ')')?
    3.27    ;
     4.1 --- a/src/Doc/Implementation/ML.thy	Wed Dec 06 14:19:36 2017 +0100
     4.2 +++ b/src/Doc/Implementation/ML.thy	Wed Dec 06 15:46:35 2017 +0100
     4.3 @@ -695,7 +695,7 @@
     4.4    @{rail \<open>
     4.5    @@{ML_antiquotation make_string}
     4.6    ;
     4.7 -  @@{ML_antiquotation print} @{syntax name}?
     4.8 +  @@{ML_antiquotation print} embedded?
     4.9    \<close>}
    4.10  
    4.11    \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to
     5.1 --- a/src/Doc/Implementation/Prelim.thy	Wed Dec 06 14:19:36 2017 +0100
     5.2 +++ b/src/Doc/Implementation/Prelim.thy	Wed Dec 06 15:46:35 2017 +0100
     5.3 @@ -142,9 +142,9 @@
     5.4    \end{matharray}
     5.5  
     5.6    @{rail \<open>
     5.7 -  @@{ML_antiquotation theory} name?
     5.8 +  @@{ML_antiquotation theory} embedded?
     5.9    ;
    5.10 -  @@{ML_antiquotation theory_context} name
    5.11 +  @@{ML_antiquotation theory_context} embedded
    5.12    \<close>}
    5.13  
    5.14    \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
    5.15 @@ -938,7 +938,7 @@
    5.16    \end{matharray}
    5.17  
    5.18    @{rail \<open>
    5.19 -  @@{ML_antiquotation binding} name
    5.20 +  @@{ML_antiquotation binding} embedded
    5.21    \<close>}
    5.22  
    5.23    \<^descr> \<open>@{binding name}\<close> produces a binding with base name \<open>name\<close> and the source
     6.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 06 14:19:36 2017 +0100
     6.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 06 15:46:35 2017 +0100
     6.3 @@ -1307,7 +1307,7 @@
     6.4    (@@{ML_antiquotation class_syntax} |
     6.5     @@{ML_antiquotation type_syntax} |
     6.6     @@{ML_antiquotation const_syntax} |
     6.7 -   @@{ML_antiquotation syntax_const}) name
     6.8 +   @@{ML_antiquotation syntax_const}) embedded
     6.9    \<close>}
    6.10  
    6.11    \<^descr> @{command parse_translation} etc. declare syntax translation functions to
     7.1 --- a/src/Doc/Isar_Ref/document/showsymbols	Wed Dec 06 14:19:36 2017 +0100
     7.2 +++ b/src/Doc/Isar_Ref/document/showsymbols	Wed Dec 06 15:46:35 2017 +0100
     7.3 @@ -5,13 +5,8 @@
     7.4  $eol = "&";
     7.5  
     7.6  while (<ARGV>) {
     7.7 -    if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) {
     7.8 -        if ($1 eq "isasym") {
     7.9 -            print "\\verb,\\<$2>, & {\\isasym$2} $eol\n";
    7.10 -        }
    7.11 -        else {
    7.12 -            print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n";
    7.13 -        }
    7.14 +    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
    7.15 +        print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
    7.16          if ("$eol" eq "&") {
    7.17              $eol = "\\\\";
    7.18          } else {
     8.1 --- a/src/Pure/ML/ml_antiquotation.ML	Wed Dec 06 14:19:36 2017 +0100
     8.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Wed Dec 06 15:46:35 2017 +0100
     8.3 @@ -41,7 +41,7 @@
     8.4    inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
     8.5  
     8.6    value (Binding.make ("binding", \<^here>))
     8.7 -    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
     8.8 +    (Scan.lift (Parse.position Args.embedded) >> ML_Syntax.make_binding) #>
     8.9  
    8.10    value (Binding.make ("cartouche", \<^here>))
    8.11      (Scan.lift Args.cartouche_input >> (fn source =>
     9.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 14:19:36 2017 +0100
     9.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 15:46:35 2017 +0100
     9.3 @@ -41,7 +41,7 @@
     9.4  
     9.5  val _ = Theory.setup
     9.6   (ML_Antiquotation.value @{binding system_option}
     9.7 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
     9.8 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
     9.9        let
    9.10          val markup =
    9.11            Options.default_markup (name, pos) handle ERROR msg =>
    9.12 @@ -57,13 +57,13 @@
    9.13        in ML_Syntax.print_string name end)) #>
    9.14  
    9.15    ML_Antiquotation.value @{binding theory}
    9.16 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    9.17 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    9.18        (Theory.check ctxt (name, pos);
    9.19         "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    9.20      || Scan.succeed "Proof_Context.theory_of ML_context") #>
    9.21  
    9.22    ML_Antiquotation.value @{binding theory_context}
    9.23 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    9.24 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    9.25        (Theory.check ctxt (name, pos);
    9.26         "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    9.27          ML_Syntax.print_string name))) #>
    9.28 @@ -85,7 +85,7 @@
    9.29      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    9.30  
    9.31    ML_Antiquotation.inline @{binding method}
    9.32 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    9.33 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    9.34        ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
    9.35  
    9.36  
    9.37 @@ -93,7 +93,7 @@
    9.38  
    9.39  val _ = Theory.setup
    9.40   (ML_Antiquotation.inline @{binding locale}
    9.41 -   (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    9.42 +   (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    9.43        Locale.check (Proof_Context.theory_of ctxt) (name, pos)
    9.44        |> ML_Syntax.print_string)));
    9.45  
    9.46 @@ -260,14 +260,14 @@
    9.47  
    9.48  val _ = Theory.setup
    9.49   (ML_Antiquotation.value @{binding keyword}
    9.50 -    (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
    9.51 +    (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true)))
    9.52        >> (fn (ctxt, (name, pos)) =>
    9.53          if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
    9.54            (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
    9.55             "Parse.$$$ " ^ ML_Syntax.print_string name)
    9.56          else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    9.57    ML_Antiquotation.value @{binding command_keyword}
    9.58 -    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
    9.59 +    (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) =>
    9.60        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
    9.61          SOME markup =>
    9.62           (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
    10.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Dec 06 14:19:36 2017 +0100
    10.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Dec 06 15:46:35 2017 +0100
    10.3 @@ -98,7 +98,7 @@
    10.4  
    10.5  val _ = Theory.setup
    10.6    (ML_Antiquotation.inline @{binding named_theorems}
    10.7 -    (Args.context -- Scan.lift (Parse.position Args.name) >>
    10.8 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >>
    10.9        (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
   10.10  
   10.11  end;
    11.1 --- a/src/Pure/Tools/plugin.ML	Wed Dec 06 14:19:36 2017 +0100
    11.2 +++ b/src/Pure/Tools/plugin.ML	Wed Dec 06 15:46:35 2017 +0100
    11.3 @@ -41,7 +41,7 @@
    11.4  
    11.5  val _ = Theory.setup
    11.6    (ML_Antiquotation.inline @{binding plugin}
    11.7 -    (Args.context -- Scan.lift (Parse.position Args.name)
    11.8 +    (Args.context -- Scan.lift (Parse.position Args.embedded)
    11.9        >> (ML_Syntax.print_string o uncurry check)));
   11.10  
   11.11  
    12.1 --- a/src/Pure/simplifier.ML	Wed Dec 06 14:19:36 2017 +0100
    12.2 +++ b/src/Pure/simplifier.ML	Wed Dec 06 15:46:35 2017 +0100
    12.3 @@ -113,7 +113,7 @@
    12.4  
    12.5  val _ = Theory.setup
    12.6    (ML_Antiquotation.value @{binding simproc}
    12.7 -    (Args.context -- Scan.lift (Parse.position Args.name)
    12.8 +    (Args.context -- Scan.lift (Parse.position Args.embedded)
    12.9        >> (fn (ctxt, name) =>
   12.10          "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
   12.11