more embedded cartouche arguments;
more uniform LaTeX output for control symbols;

--- 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}}

--- 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}}

--- 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 \<open>
-  @@{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
   \<close>}
@@ -392,7 +392,7 @@
 
   @{rail \<open>
   (@@{ML_antiquotation const_name} |
-   @@{ML_antiquotation const_abbrev}) name
+   @@{ML_antiquotation const_abbrev}) embedded
   ;
   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   ;

--- 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 \<open>
   @@{ML_antiquotation make_string}
   ;
-  @@{ML_antiquotation print} @{syntax name}?
+  @@{ML_antiquotation print} embedded?
   \<close>}
 
   \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to

--- 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 \<open>
-  @@{ML_antiquotation theory} name?
+  @@{ML_antiquotation theory} embedded?
   ;
-  @@{ML_antiquotation theory_context} name
+  @@{ML_antiquotation theory_context} embedded
   \<close>}
 
   \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
@@ -938,7 +938,7 @@
   \end{matharray}
 
   @{rail \<open>
-  @@{ML_antiquotation binding} name
+  @@{ML_antiquotation binding} embedded
   \<close>}
 
   \<^descr> \<open>@{binding name}\<close> produces a binding with base name \<open>name\<close> and the source

--- 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
   \<close>}
 
   \<^descr> @{command parse_translation} etc. declare syntax translation functions to

--- 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 (<ARGV>) {
-    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 {

--- 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 =>

--- 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)];

--- 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;

--- 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)));
 
 

--- 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))));