merged

--- a/NEWS	Wed Dec 18 16:48:14 2024 +0100
+++ b/NEWS	Wed Dec 18 23:36:51 2024 +0100
@@ -209,6 +209,16 @@
   \renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
   \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
 
+* LaTeX presentation of outer syntax keywords now distinguishes
+keyword1, keyword2, keyword3 more carefully. This allows to imitate
+Isabelle/jEdit rendering like this:
+
+  \renewcommand{\isacommand}[1]{\isakeywordONE{#1}}
+  \renewcommand{\isakeywordONE}[1]{\isakeyword{\color[RGB]{0,102,153}#1}}
+  \renewcommand{\isakeywordTWO}[1]{\isakeyword{\color[RGB]{0,153,102}#1}}
+  \renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}}
+
+
 
 *** HOL ***
 

--- a/lib/texinputs/isabelle.sty	Wed Dec 18 16:48:14 2024 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Dec 18 23:36:51 2024 +0100
@@ -151,6 +151,9 @@
 {\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
 \newcommand{\isacommand}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordONE}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTWO}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTHREE}[1]{\isakeyword{#1}}
 \newcommand{\isatclass}[1]{#1}
 \newcommand{\isatconst}[1]{#1}
 \newcommand{\isatfree}[1]{#1}

--- a/src/Pure/General/latex.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/General/latex.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -247,10 +247,10 @@
 val markup_indent = markup_macro "isaindent";
 val markup_latex =
  Symtab.make
-  [(Markup.commandN, markup_macro "isacommand"),
-   (Markup.keyword1N, markup_macro "isacommand"),
-   (Markup.keyword2N, markup_macro "isakeyword"),
-   (Markup.keyword3N, markup_macro "isacommand"),
+  [(Markup.commandN, markup_macro "isakeywordONE"),
+   (Markup.keyword1N, markup_macro "isakeywordONE"),
+   (Markup.keyword2N, markup_macro "isakeywordTWO"),
+   (Markup.keyword3N, markup_macro "isakeywordTHREE"),
    (Markup.tclassN, markup_macro "isatclass"),
    (Markup.tconstN, markup_macro "isatconst"),
    (Markup.tfreeN, markup_macro "isatfree"),

--- a/src/Pure/General/mailman.scala	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/General/mailman.scala	Wed Dec 18 23:36:51 2024 +0100
@@ -20,27 +20,27 @@
 
   private val standard_name: Map[String, String] =
     Map(
-      "[e-mail]" -> "Guo Fan\[e-mail]",
+      "121171528:qq/com" -> "Guo Fan\n121171528:qq/com",
       "Aman Pohjola, Johannes (Data61, Kensington NSW)" -> "Johannes Aman Pohjola",
       "Andrei de AraÃjo Formiga" -> "Andrei de Araujo Formiga",
-      "[e-mail]" -> "Benedikt Ahrens\[e-mail]",
+      "Benedikt/AHRENS:unice/fr" -> "Benedikt Ahrens\nBenedikt/AHRENS:unice/fr",
       "Berg, Nils Erik" -> "Nils Erik Berg",
-      "Berger U." -> "Ulrich Berger",
+      "Berger U/" -> "Ulrich Berger",
       "Bisping, Benjamin" -> "Benjamin Bisping",
-      "Blanchette, J.C." -> "Jasmin Christian Blanchette",
+      "Blanchette, J/C/" -> "Jasmin Christian Blanchette",
       "Buday Gergely István" -> "Gergely Buday",
-      "[e-mail]" -> "",
-      "CRACIUN F." -> "Florin Craciun",
+      "CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw:mail/gmail/com" -> "",
+      "CRACIUN F/" -> "Florin Craciun",
       "Carsten Schuermann" -> "Carsten Schürmann",
       "Chris" -> "",
       "Christoph Lueth" -> "Christoph Lüth",
       "Claude Marche" -> "Claude Marché",
       "Daniel StÃwe" -> "Daniel Stüwe",
-      "[e-mail]" -> "Daniel Matichuk\[e-mail]",
-      "[e-mail]" -> "Daniel Matichuk\[e-mail]",
+      "Daniel/Matichuk:data61/csiro/au" -> "Daniel Matichuk\nDaniel/Matichuk:data61/csiro/au",
+      "Daniel/Matichuk:nicta/com/au" -> "Daniel Matichuk\nDaniel/Matichuk:nicta/com/au",
       "David MENTRE" -> "David MENTRÉ",
       "Dey, Katie" -> "Katie Dey",
-      "Dr. Brendan Patrick Mahony" -> "Brendan Mahony",
+      "Dr/ Brendan Patrick Mahony" -> "Brendan Mahony",
       "Farn" -> "Farn Wang",
       "Farquhar, Colin I" -> "Colin Farquhar",
       "Fernandez, Matthew" -> "Matthew Fernandez",
@@ -50,7 +50,7 @@
       "Francisco Jose CHAVES ALONSO" -> "Francisco Jose Chaves Alonso",
       "Frederic Tuong (Dr)" -> "Frederic Tuong",
       "Fulya" -> "Fulya Horozal",
-      "George K." -> "George Karabotsos",
+      "George K/" -> "George Karabotsos",
       "Gidon Ernst" -> "Gidon ERNST",
       "Gransden, Thomas" -> "Thomas Gransden",
       "Hans-JÃrg Schurr" -> "Hans-Jörg Schurr",
@@ -58,7 +58,7 @@
       "Hitoshi Ohsaki (RTA publicity chair)" -> "Hitoshi Ohsaki",
       "Häuselmann Rafael" -> "Rafael Häuselmann",
       "Isabelle" -> "",
-      "J. Juhas (TUM)" -> "Jonatan Juhas",
+      "J/ Juhas (TUM)" -> "Jonatan Juhas",
       "Jackson, Vincent (Data61, Kensington NSW)" -> "Vincent Jackson",
       "Janney, Mark-P26816" -> "Mark Janney",
       "Jean François Molderez" -> "Jean-François Molderez",
@@ -70,7 +70,7 @@
       "Klein, Gerwin (Data61, Kensington NSW)" -> "Gerwin Klein",
       "Kobayashi, Hidetsune" -> "Hidetsune Kobayashi",
       "Kylie Williams (IND)" -> "Kylie Williams",
-      "Laarman, A.W." -> "A.W. Laarman",
+      "Laarman, A/W/" -> "A/W/ Laarman",
       "Laurent Thery" -> "Laurent Théry",
       "Li, Chanjuan" -> "Li Chanjuan",
       "Lochbihler Andreas" -> "Andreas Lochbihler",
@@ -86,7 +86,7 @@
       "Marmsoler, Diego" -> "Diego Marmsoler",
       "Martin Klebermass" -> "Martin Klebermaß",
       "Martyn Johnson via RT" -> "",
-      "[e-mail]" -> "Mathias Fleury\[e-mail]",
+      "Mathias/Fleury:ens-rennes/fr" -> "Mathias Fleury\nmathias/fleury12:gmail/com",
       "Matthew" -> "",
       "Matthews, John R" -> "John Matthews",
       "McCarthy, Jim (C3ID)" -> "Jim McCarthy",
@@ -94,10 +94,10 @@
       "Michael FÃrber" -> "Michael Färber",
       "Michel" -> "",
       "Miranda, Brando" -> "Brando Miranda",
-      "Moscato, Mariano M. \\(LARC-D320\\)\\[NATIONAL INSTITUTE OF AEROSPACE\\]" -> "Mariano M. Moscato",
+      "Moscato, Mariano M/ \\(LARC-D320\\)\\[NATIONAL INSTITUTE OF AEROSPACE\\]" -> "Mariano M/ Moscato",
       "Mr Julian Fell" -> "Julian Fell",
       "Mueller Peter" -> "Peter Müller",
-      "Munoz, Cesar Augusto (LARC-D320)" -> "Cesar A. Munoz",
+      "Munoz, Cesar Augusto (LARC-D320)" -> "Cesar A/ Munoz",
       "Nadel, Alexander" -> "Alexander Nadel",
       "Nagashima, Yutaka" -> "Yutaka Nagashima",
       "Norrish, Michael (Data61, Acton)" -> "Michael Norrish",
@@ -109,34 +109,34 @@
       "PAQUI LUCIO" -> "Paqui Lucio",
       "Pal, Abhik" -> "Abhik Pal",
       "Pasupuleti, Vijay" -> "Vijay Pasupuleti",
-      "Peter Vincent Homeier" -> "Peter V. Homeier",
+      "Peter Vincent Homeier" -> "Peter V/ Homeier",
       "Peter" -> "",
       "Philipp Ruemmer" -> "Philipp Rümmer",
       "Philipp RÃmmer" -> "Philipp Rümmer",
       "Piete Brooks via RT" -> "",
       "RTA publicity chair" -> "",
-      "Raamsdonk, F. van" -> "Femke van Raamsdonk",
+      "Raamsdonk, F/ van" -> "Femke van Raamsdonk",
       "Raul Gutierrez" -> "Raúl Gutiérrez",
       "Renà Thiemann" -> "René Thiemann",
-      "Ridgway, John V. E." -> "John V. E. Ridgway",
-      "Roggenbach M." -> "Markus Roggenbach",
+      "Ridgway, John V/ E/" -> "John V/ E/ Ridgway",
+      "Roggenbach M/" -> "Markus Roggenbach",
       "Rosu, Grigore" -> "Grigore Rosu",
       "Rozman, Mihaela" -> "Mihaela Rozman",
-      "Schmaltz, J." -> "Julien Schmaltz",
-      "Serguei A. Mokhov on behalf of PST-11" -> "Serguei A. Mokhov",
-      "Serguei Mokhov" -> "Serguei A. Mokhov",
+      "Schmaltz, J/" -> "Julien Schmaltz",
+      "Serguei A/ Mokhov on behalf of PST-11" -> "Serguei A/ Mokhov",
+      "Serguei Mokhov" -> "Serguei A/ Mokhov",
       "Shumeiko, Igor" -> "Igor Shumeiko",
       "Siek, Jeremy" -> "Jeremy Siek",
-      "[e-mail]" -> "Silvio Ranise\[e-mail]",
+      "Silvio/Ranise:loria/fr" -> "Silvio Ranise\nSilvio/Ranise:loria/fr",
       "Siu, Tony" -> "Tony Siu",
       "Stüber, Sebastian" -> "Sebastian Stüber",
       "Thiemann, Rene" -> "René Thiemann",
       "Thiemann, René" -> "René Thiemann",
       "Thomas Arthur Leck Sewell" -> "Thomas Sewell",
       "Thomas Goethel" -> "Thomas Göthel",
-      "[e-mail]" -> "Thomas Sewell\[e-mail]",
+      "Thomas/Sewell:data61/csiro/au" -> "Thomas Sewell\nThomas/Sewell:data61/csiro/au",
       "Tjark Weber via RT" -> "Tjark Weber",
-      "[e-mail]" -> "Toby Murray\[e-mail]",
+      "Toby/Murray:data61/csiro/au" -> "Toby Murray\nToby/Murray:data61/csiro/au",
       "Urban, Christian" -> "Christian Urban",
       "Ursula Eschbach" -> "",
       "Van Staden Stephan" -> "Stephan van Staden",
@@ -154,57 +154,64 @@
       "chen kun" -> "Chen Kun",
       "chunhan wu" -> "Chunhan Wu",
       "daniel de la concepción sáez" -> "Daniel de la Concepción Sáez",
-      "[e-mail]" -> "[e-mail]",
+      "daniel/luckhardt:mathematik/uni-goettingen/de" -> "Logiker:gmx/net",
       "david streader" -> "David Streader",
-      "[e-mail]" -> "",
-      "[e-mail]" -> "[e-mail]",
-      "[e-mail]" -> "[e-mail]",
-      "[e-mail]" -> "[e-mail]",
-      "gallais @ ensl.org" -> "Guillaume Allais",
+      "eschbach:in/tum/de" -> "",
+      "f/rabe:jacobs-university/de" -> "florian/rabe:fau/de",
+      "florian:haftmann-online/de" -> "haftmann:in/tum/de",
+      "fredegar:haftmann-online/de" -> "haftmann:in/tum/de",
+      "gallais : ensl/org" -> "Guillaume Allais",
       "geng chen" -> "Geng Chen",
-      "henning.seidler" -> "Henning Seidler",
+      "henning/seidler" -> "Henning Seidler",
       "hkb" -> "Hidetsune Kobayashi",
-      "[e-mail]" -> "",
-      "julien@RadboudUniversity" -> "",
+      "jobs-pm:inf/ethz/ch" -> "",
+      "julien:RadboudUniversity" -> "",
       "jun sun" -> "Jun Sun",
-      "jwang whu.edu.cn (jwang)" -> "jwang",
+      "jwang whu/edu/cn (jwang)" -> "jwang",
       "kostas pouliasis" -> "Kostas Pouliasis",
-      "[e-mail]" -> "Kristof Teichel\[e-mail]",
+      "kristof/teichel:ptb/de" -> "Kristof Teichel\nkristof/teichel:ptb/de",
       "lucas cavalcante" -> "Lucas Cavalcante",
       "mahmoud abdelazim" -> "Mahmoud Abdelazim",
       "manish surolia" -> "Manish Surolia",
       "mantel" -> "Heiko Mantel",
       "marco caminati" -> "Marco Caminati",
-      "[e-mail]" -> "Mathias Fleury\[e-mail]",
-      "[e-mail]" -> "[e-mail]",
+      "mathias/fleury:ens-rennes/fr" -> "Mathias Fleury\nmathias/fleury12:gmail/com",
+      "merz:loria/fr" -> "stephan/merz:loria/fr",
       "michel levy" -> "Michel Levy",
-      "[e-mail]" -> "Michel Levy\[e-mail]",
+      "michel/levy2009:laposte/net" -> "Michel Levy\nmichel/levy2009:laposte/net",
       "nemouchi" -> "Yakoub Nemouchi",
       "noam neer" -> "Noam Neer",
       "olfa mraihi" -> "Olfa Mraihi",
-      "[e-mail]" -> "Leo Freitas\[e-mail]",
+      "pathsnottakenworkshop:gmail/com" -> "Leo Freitas\nleo/freitas:newcastle/ac/uk",
       "patrick barlatier" -> "Patrick Barlatier",
       "patrick dabou" -> "Patrick Dabou",
       "paul zimmermann" -> "Paul Zimmermann",
-      "[e-mail]" -> "Andrei Popescu",
+      "popescu2:illinois/edu" -> "Andrei Popescu",
       "recruiting" -> "",
-      "[e-mail]" -> "",
+      "recruiting:mais/informatik/tu-darmstadt/de" -> "",
       "roux cody" -> "Cody Roux",
       "scott constable" -> "Scott Constable",
-      "[e-mail]" -> "Matthew Weidner\[e-mail]",
-      "[e-mail]" -> "Christian Urban\[e-mail]",
-      "[e-mail]" -> "[e-mail]",
+      "superuser:mattweidner/com" -> "Matthew Weidner\nsuperuser:mattweidner/com",
+      "urban:math/lmu/de" -> "Christian Urban\nurban:math/lmu/de",
+      "veronique/cortier:loria/fr" -> "Veronique/Cortier:loria/fr",
       "vikram singh" -> "Vikram Singh",
-      "[e-mail]" -> "[e-mail]",
-      "[e-mail]" -> "Benjamin Werner\[e-mail]",
-      "[e-mail]" -> "William Mansky\[e-mail]",
-      "[e-mail]" -> "Yakoub Nemouchi\[e-mail]",
+      "wenzelm:in/tum/de" -> "makarius:sketis/net",
+      "werner:lix/polytechnique/fr" -> "Benjamin Werner\nwerner:lix/polytechnique/fr",
+      "wmansky:cs/princeton/edu" -> "William Mansky\nwmansky:cs/princeton/edu",
+      "y/nemouchi:ensbiotech/edu/dz" -> "Yakoub Nemouchi\ny/nemouchi:ensbiotech/edu/dz",
       "ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ" -> "",
-      "∀X.Xπ - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
-    ).withDefault(identity)
+      "∀X/Xπ - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
+    )
+
+  private def tune(s: String): String =
+    s.replace(64.toChar, 58.toChar).replace(46.toChar, 47.toChar)
+
+  private def untune(s: String): String =
+    s.replace(58.toChar, 64.toChar).replace(47.toChar, 46.toChar)
 
   def standard_author_info(author_info: List[String]): List[String] =
-    author_info.flatMap(s => split_lines(standard_name.getOrElse(s, s))).distinct
+    author_info.flatMap(s =>
+      split_lines(standard_name.get(tune(s)).map(untune).getOrElse(s))).distinct
 
   sealed case class Message(
     name: String,

--- a/src/Pure/Isar/keyword.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -80,6 +80,7 @@
   val is_proof_open: keywords -> string -> bool
   val is_proof_close: keywords -> string -> bool
   val is_proof_asm: keywords -> string -> bool
+  val is_proof_asm_goal: keywords -> string -> bool
   val is_improper: keywords -> string -> bool
   val is_printed: keywords -> string -> bool
 end;
@@ -289,6 +290,7 @@
 val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
 
 val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_proof_asm_goal = command_category [prf_asm_goal];
 val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
 
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;

--- a/src/Pure/PIDE/markup.scala	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 18 23:36:51 2024 +0100
@@ -179,9 +179,9 @@
 
   val EXPRESSION = "expression"
   object Expression {
-    def unapply(markup: Markup): Option[String] =
+    def unapply(markup: Markup): Option[(String, String)] =
       markup match {
-        case Markup(EXPRESSION, props) => Some(Kind.get(props))
+        case Markup(EXPRESSION, props) => Some((Kind.get(props), Name.get(props)))
         case _ => None
       }
 

--- a/src/Pure/PIDE/markup_kind.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/PIDE/markup_kind.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -17,6 +17,7 @@
   val check_expression: Proof.context -> xstring * Position.T -> Markup.T
   val setup_expression: binding -> Markup.T
   val markup_item: Markup.T
+  val markup_syntax: Markup.T
   val markup_mixfix: Markup.T
   val markup_prefix: Markup.T
   val markup_postfix: Markup.T
@@ -99,6 +100,8 @@
 
 val markup_item = setup_expression (Binding.make ("item", \<^here>));
 
+val markup_syntax = setup_expression (Binding.make ("syntax", \<^here>));
+
 val markup_mixfix = setup_notation (Binding.make ("mixfix", \<^here>));
 val markup_prefix = setup_notation (Binding.make ("prefix", \<^here>));
 val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>));

--- a/src/Pure/PIDE/rendering.scala	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 18 23:36:51 2024 +0100
@@ -172,6 +172,14 @@
       Markup.TFREE -> "free type variable",
       Markup.TVAR -> "schematic type variable")
 
+  def tooltip_text(markup: String, kind: String, name: String): String = {
+    val a = kind.nonEmpty
+    val b = name.nonEmpty
+    val k = Word.implode(Word.explode('_', kind))
+    if (!a && !b) markup
+    else markup + ": " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
+  }
+
 
   /* entity focus */
 
@@ -716,18 +724,11 @@
             Some(info.add_info_text(r0, "language: " + lang.description))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
-            val a = kind.nonEmpty
-            val b = name.nonEmpty
-            val k = Word.implode(Word.explode('_', kind))
-            val description =
-              if (!a && !b) "notation"
-              else "notation: " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
+            val description = Rendering.tooltip_text(Markup.NOTATION, kind, name)
             Some(info.add_info_text(r0, description, ord = 1))
 
-          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
-            val description =
-              if (kind.isEmpty) "expression"
-              else "expression: " + Word.implode(Word.explode('_', kind))
+          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind, name), _))) =>
+            val description = Rendering.tooltip_text(Markup.EXPRESSION, kind, name)
             Some(info.add_info_text(r0, description, ord = 1))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>

--- a/src/Pure/Syntax/parser.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -543,8 +543,15 @@
   end;
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
-  | pretty_tree (Node ({const = c, ...}, ts)) =
-      [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_tree ts))]
+  | pretty_tree (Node ({nonterm = nt, const = c, ...}, ts)) =
+      let
+        fun mark_const body =
+          if c = "" then body
+          else [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: body))];
+        fun mark_nonterm body =
+          if nt = "" then body
+          else [Pretty.markup_open (Markup.name nt Markup_Kind.markup_syntax) body];
+      in mark_nonterm (mark_const (maps pretty_tree ts))  end
   | pretty_tree (Tip tok) =
       if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
 

--- a/src/Pure/Thy/document_antiquotations.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -437,7 +437,7 @@
 
 val _ =
   Theory.setup
-   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isacommand" #>
+   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isakeywordONE" #>
     entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "isa" #>
     entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "isa");
 

--- a/src/Pure/Thy/document_output.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/Pure/Thy/document_output.ML	Wed Dec 18 23:36:51 2024 +0100
@@ -159,16 +159,27 @@
 
 fun output_token ctxt tok =
   let
+    val keywords = Thy_Header.get_keywords' ctxt;
+
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   in
     (case Token.kind_of tok of
       Token.Comment NONE => []
     | Token.Comment (SOME Comment.Marker) => []
-    | Token.Command => output false "\\isacommand{" "}"
+    | Token.Command =>
+        let
+          val name = (Token.content_of tok);
+          val bg =
+            if Keyword.is_theory_end keywords name then "\\isakeywordTWO{"
+            else if Keyword.is_proof_asm keywords name orelse
+              Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+            else if Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+            else "\\isakeywordONE{";
+        in output false bg "}" end
     | Token.Keyword =>
         if Symbol.is_ascii_identifier (Token.content_of tok)
-        then output false "\\isakeyword{" "}"
+        then output false "\\isakeywordTWO{" "}"
         else output false "" ""
     | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"