# HG changeset patch
# User wenzelm
# Date 1445366733 -7200
# Node ID 97261e6c1d423f5c9164fcf9c61e51b55db10c87
# Parent  7c9c54eb9658c806612284ba2ecb4d2f965f3722
another antiquotation short form: undecorated cartouche as alias for @{text};
document antiquotation @{text} ignores option "source";

diff -r 7c9c54eb9658 -r 97261e6c1d42 NEWS
--- 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.
diff -r 7c9c54eb9658 -r 97261e6c1d42 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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
diff -r 7c9c54eb9658 -r 97261e6c1d42 src/Pure/General/antiquote.ML
--- 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 --
diff -r 7c9c54eb9658 -r 97261e6c1d42 src/Pure/General/antiquote.scala
--- 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))
diff -r 7c9c54eb9658 -r 97261e6c1d42 src/Pure/ML/ml_lex.ML
--- 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 =
diff -r 7c9c54eb9658 -r 97261e6c1d42 src/Pure/Thy/thy_output.ML
--- 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);