# HG changeset patch # User wenzelm # Date 1734561411 -3600 # Node ID 633fa7a4bf30a81a955ea24c802f7d74f94141c7 # Parent 24c1edcbcc6b4c4c13f4ce7fca1ebf0290d8dcdd# Parent 2d4838ffb67e2e1350e05acfe4b31a709587c4c2 merged diff -r 24c1edcbcc6b -r 633fa7a4bf30 NEWS --- 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 *** diff -r 24c1edcbcc6b -r 633fa7a4bf30 lib/texinputs/isabelle.sty --- 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} diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/General/latex.ML --- 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"), diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/General/mailman.scala --- 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( - "121171528@qq.com" -> "Guo Fan\n121171528@qq.com", + "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", - "Benedikt.AHRENS@unice.fr" -> "Benedikt Ahrens\nBenedikt.AHRENS@unice.fr", + "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", - "CALaF1UJ9Uy0vGCu4WkBmbfuPDxG7nFm8hfeCMP+O3g7_5CQ0Bw@mail.gmail.com" -> "", - "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", - "Daniel.Matichuk@data61.csiro.au" -> "Daniel Matichuk\nDaniel.Matichuk@data61.csiro.au", - "Daniel.Matichuk@nicta.com.au" -> "Daniel Matichuk\nDaniel.Matichuk@nicta.com.au", + "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" -> "", - "Mathias.Fleury@ens-rennes.fr" -> "Mathias Fleury\nmathias.fleury12@gmail.com", + "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", - "Silvio.Ranise@loria.fr" -> "Silvio Ranise\nSilvio.Ranise@loria.fr", + "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", - "Thomas.Sewell@data61.csiro.au" -> "Thomas Sewell\nThomas.Sewell@data61.csiro.au", + "Thomas/Sewell:data61/csiro/au" -> "Thomas Sewell\nThomas/Sewell:data61/csiro/au", "Tjark Weber via RT" -> "Tjark Weber", - "Toby.Murray@data61.csiro.au" -> "Toby Murray\nToby.Murray@data61.csiro.au", + "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", - "daniel.luckhardt@mathematik.uni-goettingen.de" -> "Logiker@gmx.net", + "daniel/luckhardt:mathematik/uni-goettingen/de" -> "Logiker:gmx/net", "david streader" -> "David Streader", - "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", + "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", - "jobs-pm@inf.ethz.ch" -> "", - "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", - "kristof.teichel@ptb.de" -> "Kristof Teichel\nkristof.teichel@ptb.de", + "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", - "mathias.fleury@ens-rennes.fr" -> "Mathias Fleury\nmathias.fleury12@gmail.com", - "merz@loria.fr" -> "stephan.merz@loria.fr", + "mathias/fleury:ens-rennes/fr" -> "Mathias Fleury\nmathias/fleury12:gmail/com", + "merz:loria/fr" -> "stephan/merz:loria/fr", "michel levy" -> "Michel Levy", - "michel.levy2009@laposte.net" -> "Michel Levy\nmichel.levy2009@laposte.net", + "michel/levy2009:laposte/net" -> "Michel Levy\nmichel/levy2009:laposte/net", "nemouchi" -> "Yakoub Nemouchi", "noam neer" -> "Noam Neer", "olfa mraihi" -> "Olfa Mraihi", - "pathsnottakenworkshop@gmail.com" -> "Leo Freitas\nleo.freitas@newcastle.ac.uk", + "pathsnottakenworkshop:gmail/com" -> "Leo Freitas\nleo/freitas:newcastle/ac/uk", "patrick barlatier" -> "Patrick Barlatier", "patrick dabou" -> "Patrick Dabou", "paul zimmermann" -> "Paul Zimmermann", - "popescu2@illinois.edu" -> "Andrei Popescu", + "popescu2:illinois/edu" -> "Andrei Popescu", "recruiting" -> "", - "recruiting@mais.informatik.tu-darmstadt.de" -> "", + "recruiting:mais/informatik/tu-darmstadt/de" -> "", "roux cody" -> "Cody Roux", "scott constable" -> "Scott Constable", - "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", + "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", - "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", + "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, diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/Isar/keyword.ML --- 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; diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/PIDE/markup.scala --- 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 } diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/PIDE/markup_kind.ML --- 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>)); diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/PIDE/rendering.scala --- 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, _), _))) => diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/Syntax/parser.ML --- 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 []; diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/Thy/document_antiquotations.ML --- 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>\command\ Outer_Syntax.check_command "isacommand" #> + (entity_antiquotation \<^binding>\command\ Outer_Syntax.check_command "isakeywordONE" #> entity_antiquotation \<^binding>\method\ Method.check_name "isa" #> entity_antiquotation \<^binding>\attribute\ Attrib.check_name "isa"); diff -r 24c1edcbcc6b -r 633fa7a4bf30 src/Pure/Thy/document_output.ML --- 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}"