# HG changeset patch # User wenzelm # Date 1445192909 -7200 # Node ID 34d1913f0b208c865246af02780da2e89e700dd7 # Parent 6458760261caa35132190d6cdd1e42f7e066a4d8 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned; diff -r 6458760261ca -r 34d1913f0b20 NEWS --- a/NEWS Sun Oct 18 18:09:48 2015 +0200 +++ b/NEWS Sun Oct 18 20:28:29 2015 +0200 @@ -22,8 +22,8 @@ * Toplevel theorem statement 'proposition' is another alias for 'theorem'. -* There is a new short form of antiquotations: \<^foo>\...\ is -equivalent to @{"\<^foo>" \...\} for control symbols. +* There is a new short form for antiquotations with a single argument +that is a cartouche: \<^name>\...\ is equivalent to @{name \...\}. *** Prover IDE -- Isabelle/Scala/jEdit *** @@ -82,6 +82,10 @@ 'text' (with antiquotations and control symbols). The key difference is the lack of the surrounding isabelle markup environment in output. +* Document antiquotations @{emph} and @{bold} output LaTeX source +recursively, adding appropriate text style markup. These are typically +used in the short form \<^emph>\...\ and \<^bold>\...\. + *** Isar *** diff -r 6458760261ca -r 34d1913f0b20 etc/symbols --- a/etc/symbols Sun Oct 18 18:09:48 2015 +0200 +++ b/etc/symbols Sun Oct 18 20:28:29 2015 +0200 @@ -359,7 +359,7 @@ \<^item> code: 0x0025aa group: control font: IsabelleText \<^enum> code: 0x0025b8 group: control font: IsabelleText \<^descr> code: 0x0027a7 group: control font: IsabelleText -#\<^emph> code: 0x002217 group: control font: IsabelleText +\<^emph> code: 0x002217 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText diff -r 6458760261ca -r 34d1913f0b20 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Sun Oct 18 18:09:48 2015 +0200 +++ b/lib/texinputs/isabelle.sty Sun Oct 18 20:28:29 2015 +0200 @@ -44,6 +44,7 @@ \def\isactrlmedskip{\medskip} \def\isactrlbigskip{\bigskip} +\newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}} \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} \newdimen\isa@parindent\newdimen\isa@parskip diff -r 6458760261ca -r 34d1913f0b20 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 20:28:29 2015 +0200 @@ -81,7 +81,6 @@ text \ \begin{matharray}{rcl} - @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ @{antiquotation_def "theory"} & : & @{text antiquotation} \\ @{antiquotation_def "thm"} & : & @{text antiquotation} \\ @{antiquotation_def "lemma"} & : & @{text antiquotation} \\ @@ -104,10 +103,13 @@ @{antiquotation_def ML_type} & : & @{text antiquotation} \\ @{antiquotation_def ML_structure} & : & @{text antiquotation} \\ @{antiquotation_def ML_functor} & : & @{text antiquotation} \\ + @{antiquotation_def emph} & : & @{text antiquotation} \\ + @{antiquotation_def bold} & : & @{text antiquotation} \\ @{antiquotation_def verbatim} & : & @{text antiquotation} \\ @{antiquotation_def "file"} & : & @{text antiquotation} \\ @{antiquotation_def "url"} & : & @{text antiquotation} \\ @{antiquotation_def "cite"} & : & @{text antiquotation} \\ + @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ \end{matharray} The overall content of an Isabelle/Isar theory may alternate between @@ -132,16 +134,14 @@ \<^medskip> Antiquotations are in general written @{verbatim "@{"}@{text "name [options] arguments"}@{verbatim "}"}. The short form @{verbatim - "\<^control>"}@{text "\argument\"} (without surrounding @{verbatim - "@{"}@{text "\"}@{verbatim "}"}) works where the name is a single control - symbol and the argument a single cartouche. + "\<^name>"}@{text "\argument\"} (without surrounding @{verbatim + "@{"}@{text "\"}@{verbatim "}"}) works for a single argument that is a + cartouche. @{rail \ - @@{command print_antiquotations} ('!'?) - ; @{syntax_def antiquotation}: - '@{' antiquotation_body '}' | - @{syntax_ref control_symbol} @{syntax_ref cartouche} + '@' '{' antiquotation_body '}' | + '\\' '<' '^' @{syntax_ref name} '>' @{syntax_ref cartouche} \} %% FIXME less monolithic presentation, move to individual sections!? @@ -172,6 +172,8 @@ @@{antiquotation ML_type} options @{syntax text} | @@{antiquotation ML_structure} options @{syntax text} | @@{antiquotation ML_functor} options @{syntax text} | + @@{antiquotation emph} options @{syntax text} | + @@{antiquotation bold} options @{syntax text} | @@{antiquotation verbatim} options @{syntax text} | @@{antiquotation "file"} options @{syntax name} | @@{antiquotation file_unchecked} options @{syntax name} | @@ -185,16 +187,14 @@ styles: '(' (style + ',') ')' ; style: (@{syntax name} +) + ; + @@{command print_antiquotations} ('!'?) \} Note that the syntax of antiquotations may \emph{not} include source comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim text @{verbatim "{*"}~@{text "\"}~@{verbatim "*}"}. - \<^descr> @{command "print_antiquotations"} prints all document antiquotations - that are defined in the current context; the ``@{text "!"}'' option - indicates extra verbosity. - \<^descr> @{text "@{theory A}"} prints the name @{text "A"}, which is guaranteed to refer to a valid ancestor theory in the current context. @@ -266,6 +266,12 @@ check text @{text s} as ML value, infix operator, type, structure, and functor respectively. The source is printed verbatim. + \<^descr> @{text "@{emph s}"} prints document source recursively, with {\LaTeX} + markup @{verbatim \\emph{\}@{text "\"}@{verbatim \}\}. + + \<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX} + markup @{verbatim \\textbf{\}@{text "\"}@{verbatim \}\}. + \<^descr> @{text "@{verbatim s}"} prints uninterpreted source text literally as ASCII characters, using some type-writer font style. @@ -292,6 +298,10 @@ @{antiquotation_option_def cite_macro}, or the configuration option @{attribute cite_macro} in the context. For example, @{text "@{cite [cite_macro = nocite] foobar}"} produces @{verbatim \\nocite{foobar}\}. + + \<^descr> @{command "print_antiquotations"} prints all document antiquotations + that are defined in the current context; the ``@{text "!"}'' option + indicates extra verbosity. \ diff -r 6458760261ca -r 34d1913f0b20 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Oct 18 20:28:29 2015 +0200 @@ -114,7 +114,6 @@ @{syntax_def cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\"} @{verbatim "*}"} \\[1ex] - @{text control_symbol} & = & @{verbatim \\\}@{verbatim "<^"}@{text ident}@{verbatim ">"} \\ @{text letter} & = & @{text "latin | "}@{verbatim \\\}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim \\\}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\ @{text subscript} & = & @{verbatim "\<^sub>"} \\ @{text quasiletter} & = & @{text "letter | digit | "}@{verbatim "_"}@{text " | "}@{verbatim "'"} \\ diff -r 6458760261ca -r 34d1913f0b20 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Pure/General/antiquote.ML Sun Oct 18 20:28:29 2015 +0200 @@ -6,14 +6,14 @@ signature ANTIQUOTE = sig - type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} - datatype 'a antiquote = - Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq + type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list} + type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list} + datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq type text_antiquote = Symbol_Pos.T list antiquote val range: text_antiquote list -> Position.range val split_lines: text_antiquote list -> text_antiquote list list val antiq_reports: 'a antiquote list -> Position.report list - val scan_control: Symbol_Pos.T list -> (Symbol_Pos.T * Symbol_Pos.T list) * Symbol_Pos.T list + val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list val read': Position.T -> Symbol_Pos.T list -> text_antiquote list @@ -25,15 +25,15 @@ (* datatype antiquote *) -type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; -datatype 'a antiquote = - Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq; +type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}; +type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}; +datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq; type text_antiquote = Symbol_Pos.T list antiquote; fun antiquote_range (Text ss) = Symbol_Pos.range ss - | antiquote_range (Control (s, ss)) = Symbol_Pos.range (s :: ss) - | antiquote_range (Antiq (_, {range, ...})) = range; + | antiquote_range (Control {range, ...}) = range + | antiquote_range (Antiq {range, ...}) = range; fun range ants = if null ants then Position.no_range @@ -60,8 +60,8 @@ fun antiq_reports ants = ants |> maps (fn Text _ => [] - | Control (s, ss) => [(#1 (Symbol_Pos.range (s :: ss)), Markup.antiquoted)] - | Antiq (_, {start, stop, range = (pos, _)}) => + | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)] + | Antiq {start, stop, range = (pos, _), ...} => [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted), @@ -91,17 +91,22 @@ val scan_control = Scan.one (Symbol.is_control o Symbol_Pos.symbol) -- - (Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2); + Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> + (fn ((control, pos), (_, body)) => + let + val Symbol.Ctrl name = Symbol.decode control; + val range = Symbol_Pos.range ((control, pos) :: body); + in {name = (name, pos), range = range, body = body} end); val scan_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") - (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) - >> (fn (pos1, (pos2, ((body, pos3), pos4))) => - (flat body, - {start = Position.set_range (pos1, pos2), - stop = Position.set_range (pos3, pos4), - range = Position.range pos1 pos4})); + (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> + (fn (pos1, (pos2, ((body, pos3), pos4))) => + {start = Position.set_range (pos1, pos2), + stop = Position.set_range (pos3, pos4), + range = Position.range pos1 pos4, + body = flat body}); val scan_antiquote = scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text; diff -r 6458760261ca -r 34d1913f0b20 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Pure/ML/ml_context.ML Sun Oct 18 20:28:29 2015 +0200 @@ -169,12 +169,11 @@ ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt; in (decl #> tokenize range, ctxt') end else (K ([], [tok]), ctxt) - | expand (Antiquote.Control (s, ss)) ctxt = - let val range = Symbol_Pos.range (s :: ss) - in expand_src range (Token.src s [Token.read_cartouche ss]) ctxt end - | expand (Antiquote.Antiq (ss, {range, ...})) ctxt = - let val keywords = Thy_Header.get_keywords' ctxt - in expand_src range (Token.read_antiq keywords antiq (ss, #1 range)) ctxt end; + | expand (Antiquote.Control {name, range, body}) ctxt = + expand_src range (Token.src name [Token.read_cartouche body]) ctxt + | expand (Antiquote.Antiq {range, body, ...}) ctxt = + expand_src range + (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt; val ctxt = (case opt_ctxt of diff -r 6458760261ca -r 34d1913f0b20 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Pure/Thy/latex.ML Sun Oct 18 20:28:29 2015 +0200 @@ -112,10 +112,12 @@ val output_syms_antiq = (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) - | Antiquote.Control (s, ss) => output_symbols (map Symbol_Pos.symbol (s :: ss)) - | Antiquote.Antiq (ss, _) => + | Antiquote.Control {name = (name, _), body, ...} => + "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^ + output_symbols (map Symbol_Pos.symbol body) + | Antiquote.Antiq {body, ...} => enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" - (output_symbols (map Symbol_Pos.symbol ss))); + (output_symbols (map Symbol_Pos.symbol body))); val output_ctrl_symbols = implode o map output_ctrl_sym; diff -r 6458760261ca -r 34d1913f0b20 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Pure/Thy/thy_output.ML Sun Oct 18 20:28:29 2015 +0200 @@ -176,9 +176,9 @@ in fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss - | eval_antiquote state (Antiquote.Control (control, arg)) = - eval_antiq state ([], Token.src control [Token.read_cartouche arg]) - | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) = + | eval_antiquote state (Antiquote.Control {name, body, ...}) = + eval_antiq state ([], Token.src name [Token.read_cartouche body]) + | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) = let val keywords = (case try Toplevel.presentation_context_of state of @@ -186,7 +186,7 @@ | NONE => error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)); - in eval_antiq state (Token.read_antiq keywords antiq (ss, pos)) end; + in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end; end; @@ -241,7 +241,6 @@ | Markup_Env_Token of string * Input.source | Raw_Token of Input.source; - fun basic_token pred (Basic_Token tok) = pred tok | basic_token _ _ = false; @@ -606,6 +605,24 @@ (** concrete antiquotations **) +(* control style *) + +local + +fun control_antiquotation name s1 s2 = + antiquotation name (Scan.lift Args.cartouche_input) + (fn {state, ...} => enclose s1 s2 o output_text state {markdown = false}); + +in + +val _ = + Theory.setup + (control_antiquotation @{binding "emph"} "\\emph{" "}" #> + control_antiquotation @{binding "bold"} "\\textbf{" "}"); + +end; + + (* basic entities *) local diff -r 6458760261ca -r 34d1913f0b20 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Sun Oct 18 18:09:48 2015 +0200 +++ b/src/Pure/Tools/rail.ML Sun Oct 18 20:28:29 2015 +0200 @@ -85,8 +85,8 @@ fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))]; -fun antiq_token (antiq as (ss, {range, ...})) = - [Token (range, (Antiq antiq, Symbol_Pos.content ss))]; +fun antiq_token antiq = + [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))]; val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);