another antiquotation short form: undecorated cartouche as alias for @{text};
document antiquotation @{text} ignores option "source";
--- a/NEWS Mon Oct 19 23:07:17 2015 +0200
+++ b/NEWS Tue Oct 20 20:45:33 2015 +0200
@@ -22,9 +22,6 @@
* Toplevel theorem statement 'proposition' is another alias for
'theorem'.
-* 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 ***
@@ -63,6 +60,19 @@
*** Document preparation ***
+* 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>} and
+\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
+
+* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
+Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
+text.
+
+* The @{text} antiquotation now ignores the antiquotation option
+"source". The given text content is output unconditionally, without any
+surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
+argument where they are really intended, e.g. @{text \<open>"foo"\<close>}.
+
* HTML presentation uses the standard IsabelleText font and Unicode
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
print mode "HTML" loses its special meaning.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 19 23:07:17 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue Oct 20 20:45:33 2015 +0200
@@ -131,25 +131,45 @@
antiquotations are checked within the current theory or proof
context.
- \<^medskip>
- Antiquotations are in general written @{verbatim "@{"}@{text "name
- [options] arguments"}@{verbatim "}"}. The short form @{verbatim
- \<open>\\<close>}@{verbatim "<^"}@{text name}@{verbatim ">"}@{text
- "\<open>argument_content\<close>"} (without surrounding @{verbatim "@{"}@{text
- "\<dots>"}@{verbatim "}"}) works for a single argument that is a cartouche.
+ \<^medskip> Antiquotations are in general written as @{verbatim "@{"}@{text
+ "name"}~@{verbatim "["}@{text options}@{verbatim "]"}~@{text
+ "arguments"}@{verbatim "}"}. The short form @{verbatim \<open>\\<close>}@{verbatim
+ "<^"}@{text name}@{verbatim ">"}@{text "\<open>argument_content\<close>"} (without
+ surrounding @{verbatim "@{"}@{text "\<dots>"}@{verbatim "}"}) works for a single
+ argument that is a cartouche.
+
+ Omitting the control symbol is also possible: a cartouche without special
+ decoration is equivalent to @{verbatim \<open>\\<close>}@{verbatim
+ "<^cartouche>"}@{text "\<open>argument_content\<close>"}, which is equivalent to
+ @{verbatim "@{cartouche"}~@{text "\<open>argument_content\<close>"}@{verbatim "}"}. The
+ special name @{antiquotation_def cartouche} is defined in the context:
+ Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
+ (see below). Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal
+ quasi-formal text (unchecked).
\begingroup
\def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
@{rail \<open>
@{syntax_def antiquotation}:
'@{' antiquotation_body '}' |
- '\<controlstart>' @{syntax_ref name} '>' @{syntax_ref cartouche}
+ '\<controlstart>' @{syntax_ref name} '>' @{syntax_ref cartouche} |
+ @{syntax_ref cartouche}
+ ;
+ options: '[' (option * ',') ']'
+ ;
+ option: @{syntax name} | @{syntax name} '=' @{syntax name}
+ ;
\<close>}
\endgroup
+ Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source
+ comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
+ text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
+
%% FIXME less monolithic presentation, move to individual sections!?
@{rail \<open>
@{syntax_def antiquotation_body}:
+ (@@{antiquotation text} | @@{antiquotation cartouche}) options @{syntax text} |
@@{antiquotation theory} options @{syntax name} |
@@{antiquotation thm} options styles @{syntax thmrefs} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@ -162,8 +182,7 @@
@@{antiquotation abbrev} options @{syntax term} |
@@{antiquotation typ} options @{syntax type} |
@@{antiquotation type} options @{syntax name} |
- @@{antiquotation class} options @{syntax name} |
- @@{antiquotation text} options @{syntax text}
+ @@{antiquotation class} options @{syntax name}
;
@{syntax antiquotation}:
@@{antiquotation goals} options |
@@ -183,10 +202,6 @@
@@{antiquotation url} options @{syntax name} |
@@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
;
- options: '[' (option * ',') ']'
- ;
- option: @{syntax name} | @{syntax name} '=' @{syntax name}
- ;
styles: '(' (style + ',') ')'
;
style: (@{syntax name} +)
@@ -194,9 +209,14 @@
@@{command print_antiquotations} ('!'?)
\<close>}
- Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source
- comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
- text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
+ \<^descr> @{text "@{text s}"} prints uninterpreted source text @{text
+ s}. This is particularly useful to print portions of text according
+ to the Isabelle document style, without demanding well-formedness,
+ e.g.\ small pieces of terms that should not be parsed or
+ type-checked yet.
+
+ It is also possible to write this in the short form \<open>\<open>s\<close>\<close> without any
+ further decoration.
\<^descr> @{text "@{theory A}"} prints the name @{text "A"}, which is
guaranteed to refer to a valid ancestor theory in the current
@@ -236,12 +256,6 @@
\<^descr> @{text "@{class c}"} prints a class @{text c}.
- \<^descr> @{text "@{text s}"} prints uninterpreted source text @{text
- s}. This is particularly useful to print portions of text according
- to the Isabelle document style, without demanding well-formedness,
- e.g.\ small pieces of terms that should not be parsed or
- type-checked yet.
-
\<^descr> @{text "@{goals}"} prints the current \<^emph>\<open>dynamic\<close> goal
state. This is mainly for support of tactic-emulation scripts
within Isar. Presentation of goal states does not conform to the
--- a/src/Pure/General/antiquote.ML Mon Oct 19 23:07:17 2015 +0200
+++ b/src/Pure/General/antiquote.ML Tue Oct 20 20:45:33 2015 +0200
@@ -78,7 +78,8 @@
val scan_txt =
Scan.repeats1
- (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
+ (Scan.many1 (fn (s, _) =>
+ not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
$$$ "@" --| Scan.ahead (~$$ "{"));
@@ -87,16 +88,20 @@
Symbol_Pos.scan_cartouche err_prefix ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
+fun control_name sym = (case Symbol.decode sym of Symbol.Control name => name);
+
in
val scan_control =
- Scan.one (Symbol.is_control o Symbol_Pos.symbol) --
+ Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
Symbol_Pos.scan_cartouche err_prefix >>
- (fn ((control, pos), body) =>
+ (fn (opt_control, body) =>
let
- val Symbol.Control name = Symbol.decode control;
- val range = Symbol_Pos.range ((control, pos) :: body);
- in {name = (name, pos), range = range, body = body} end);
+ val (name, range) =
+ (case opt_control of
+ SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body))
+ | NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body));
+ in {name = name, range = range, body = body} end);
val scan_antiq =
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
--- a/src/Pure/General/antiquote.scala Mon Oct 19 23:07:17 2015 +0200
+++ b/src/Pure/General/antiquote.scala Tue Oct 20 20:45:33 2015 +0200
@@ -25,12 +25,12 @@
trait Parsers extends Scan.Parsers
{
private val txt: Parser[String] =
- rep1(many1(s => !Symbol.is_control(s) && s != "@") |
+ rep1(many1(s => !Symbol.is_control(s) && !Symbol.is_open(s) && s != "@") |
one(Symbol.is_control) <~ guard(opt_term(one(s => !Symbol.is_open(s)))) |
"@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
val control: Parser[String] =
- one(Symbol.is_control) ~ cartouche ^^ { case x ~ y => x + y }
+ opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x }
val antiq_other: Parser[String] =
many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
--- a/src/Pure/ML/ml_lex.ML Mon Oct 19 23:07:17 2015 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Oct 20 20:45:33 2015 +0200
@@ -293,9 +293,9 @@
val scan_sml = scan_ml >> Antiquote.Text;
val scan_ml_antiq =
+ Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) ||
Antiquote.scan_control >> Antiquote.Control ||
Antiquote.scan_antiq >> Antiquote.Antiq ||
- Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) ||
scan_ml >> Antiquote.Text;
fun recover msg =
--- a/src/Pure/Thy/thy_output.ML Mon Oct 19 23:07:17 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Oct 20 20:45:33 2015 +0200
@@ -617,8 +617,26 @@
val _ =
Theory.setup
- (control_antiquotation @{binding "emph"} "\\emph{" "}" #>
- control_antiquotation @{binding "bold"} "\\textbf{" "}");
+ (control_antiquotation @{binding emph} "\\emph{" "}" #>
+ control_antiquotation @{binding bold} "\\textbf{" "}");
+
+end;
+
+
+(* quasi-formal text (unchecked) *)
+
+local
+
+fun text_antiquotation name =
+ antiquotation name (Scan.lift Args.text_input)
+ (fn {context = ctxt, ...} => output ctxt o single o pretty_text_report ctxt);
+
+in
+
+val _ =
+ Theory.setup
+ (text_antiquotation @{binding text} #>
+ text_antiquotation @{binding cartouche});
end;
@@ -628,13 +646,13 @@
local
fun basic_entities name scan pretty =
- antiquotation name scan (fn {source, context, ...} =>
- output context o maybe_pretty_source pretty context source);
+ antiquotation name scan (fn {source, context = ctxt, ...} =>
+ output ctxt o maybe_pretty_source pretty ctxt source);
fun basic_entities_style name scan pretty =
- antiquotation name scan (fn {source, context, ...} => fn (style, xs) =>
- output context
- (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
+ antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) =>
+ output ctxt
+ (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
fun basic_entity name scan = basic_entities name (scan >> single);
@@ -651,7 +669,6 @@
basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
- basic_entity @{binding text} (Scan.lift Args.text_input) pretty_text_report #>
basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);