clarified control antiquotations: decode control symbol to get name;
document antiquotations @{emph}, @{bold};
symbol interpretation for \<^emph>;
tuned;
--- 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>\<open>...\<close> is
-equivalent to @{"\<^foo>" \<open>...\<close>} for control symbols.
+* There is a new short form for antiquotations with a single argument
+that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>}.
*** 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>\<open>...\<close> and \<^bold>\<open>...\<close>.
+
*** Isar ***
--- 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
--- 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
--- 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 \<open>
\begin{matharray}{rcl}
- @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
@{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 \<rightarrow> "} \\
\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 "\<open>argument\<close>"} (without surrounding @{verbatim
- "@{"}@{text "\<dots>"}@{verbatim "}"}) works where the name is a single control
- symbol and the argument a single cartouche.
+ "\<^name>"}@{text "\<open>argument\<close>"} (without surrounding @{verbatim
+ "@{"}@{text "\<dots>"}@{verbatim "}"}) works for a single argument that is a
+ cartouche.
@{rail \<open>
- @@{command print_antiquotations} ('!'?)
- ;
@{syntax_def antiquotation}:
- '@{' antiquotation_body '}' |
- @{syntax_ref control_symbol} @{syntax_ref cartouche}
+ '@' '{' antiquotation_body '}' |
+ '\\' '<' '^' @{syntax_ref name} '>' @{syntax_ref cartouche}
\<close>}
%% 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} ('!'?)
\<close>}
Note that the syntax of antiquotations may \emph{not} include source
comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
text @{verbatim "{*"}~@{text "\<dots>"}~@{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 \<open>\emph{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
+
+ \<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX}
+ markup @{verbatim \<open>\textbf{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
+
\<^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 \<open>\nocite{foobar}\<close>}.
+
+ \<^descr> @{command "print_antiquotations"} prints all document antiquotations
+ that are defined in the current context; the ``@{text "!"}'' option
+ indicates extra verbosity.
\<close>
--- 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 "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex]
- @{text control_symbol} & = & @{verbatim \<open>\\<close>}@{verbatim "<^"}@{text ident}@{verbatim ">"} \\
@{text letter} & = & @{text "latin | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\
@{text subscript} & = & @{verbatim "\<^sub>"} \\
@{text quasiletter} & = & @{text "letter | digit | "}@{verbatim "_"}@{text " | "}@{verbatim "'"} \\
--- 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;
--- 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
--- 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;
--- 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
--- 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);