# HG changeset patch
# User wenzelm
# Date 1397058849 -7200
# Node ID 7e0178c84994bf3807e1f2321fc7f60458c28b96
# Parent  6437c989a744e7918edd284476db5eb8e4c590e4
allow text cartouches in regular outer syntax categories "text" and "altstring";

diff -r 6437c989a744 -r 7e0178c84994 NEWS
--- a/NEWS	Wed Apr 09 17:29:37 2014 +0200
+++ b/NEWS	Wed Apr 09 17:54:09 2014 +0200
@@ -25,6 +25,10 @@
 supports input methods via ` (backquote), or << and >> (double angle
 brackets).
 
+* The outer syntax categories "text" (for formal comments and document
+markup commands) and "altstring" (for literal fact references) allow
+cartouches as well, in addition to the traditional mix of quotations.
+
 * More static checking of proof methods, which allows the system to
 form a closure over the concrete syntax.  Method arguments should be
 processed in the original proof context as far as possible, before
diff -r 6437c989a744 -r 7e0178c84994 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 09 17:29:37 2014 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Apr 09 17:54:09 2014 +0200
@@ -265,14 +265,14 @@
 
 text {* Large chunks of plain @{syntax text} are usually given
   @{syntax verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
-  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}.  For convenience,
-  any of the smaller text units conforming to @{syntax nameref} are
-  admitted as well.  A marginal @{syntax comment} is of the form
-  @{verbatim "--"}~@{syntax text}.  Any number of these may occur
-  within Isabelle/Isar commands.
+  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}, or as @{syntax
+  cartouche} @{text "\<open>\<dots>\<close>"}.  For convenience, any of the smaller text
+  units conforming to @{syntax nameref} are admitted as well.  A
+  marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax
+  text}.  Any number of these may occur within Isabelle/Isar commands.
 
   @{rail \<open>
-    @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
+    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
     ;
     @{syntax_def comment}: '--' @{syntax text}
   \<close>}
@@ -424,9 +424,9 @@
 
   \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
 
-  \item literal fact propositions using @{syntax_ref altstring} syntax
-  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
-  @{method_ref fact}).
+  \item literal fact propositions using token syntax @{syntax_ref altstring}
+  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
+  @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
 
   \end{enumerate}
 
@@ -451,7 +451,8 @@
     @{syntax_def thmdef}: thmbind '='
     ;
     @{syntax_def thmref}:
-      (@{syntax nameref} selection? | @{syntax altstring}) @{syntax attributes}? |
+      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
+        @{syntax attributes}? |
       '[' @{syntax attributes} ']'
     ;
     @{syntax_def thmrefs}: @{syntax thmref} +
diff -r 6437c989a744 -r 7e0178c84994 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 17:29:37 2014 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 17:54:09 2014 +0200
@@ -7,6 +7,29 @@
   "text_cartouche" :: thy_decl
 begin
 
+subsection {* Regular outer syntax *}
+
+text \<open>Text cartouches may be used in the outer syntax category "text",
+  as alternative to the traditional "verbatim" tokens.  An example is
+  this text block.\<close>  -- \<open>The same works for small side-comments.\<close>
+
+notepad
+begin
+  txt \<open>Moreover, cartouches work as additional syntax in the
+    "altstring" category, for literal fact references.  For example:\<close>
+
+  fix x y :: 'a
+  assume "x = y"
+  note \<open>x = y\<close>
+  have "x = y" by (rule \<open>x = y\<close>)
+  from \<open>x = y\<close> have "x = y" .
+
+  txt \<open>Of course, this can be nested inside formal comments and
+    antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
+    [OF \<open>x = y\<close>]}.\<close>
+end
+
+
 subsection {* Outer syntax: cartouche within command syntax *}
 
 ML {*
diff -r 6437c989a744 -r 7e0178c84994 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Apr 09 17:29:37 2014 +0200
+++ b/src/Pure/Isar/args.ML	Wed Apr 09 17:54:09 2014 +0200
@@ -152,7 +152,7 @@
     Parse.type_ident || Parse.type_var || Parse.number);
 
 val string = Parse.token (Parse.string || Parse.verbatim);
-val alt_string = Parse.token Parse.alt_string;
+val alt_string = Parse.token (Parse.alt_string || Parse.cartouche);
 val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic);
 
 fun $$$ x =
diff -r 6437c989a744 -r 7e0178c84994 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Apr 09 17:29:37 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Apr 09 17:54:09 2014 +0200
@@ -275,7 +275,7 @@
   (short_ident || long_ident || sym_ident || string || number);
 
 val text = group (fn () => "text")
-  (short_ident || long_ident || sym_ident || string || number || verbatim);
+  (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
 
 val path = group (fn () => "file name/path specification") name;
 
@@ -386,7 +386,7 @@
 
 val const = inner_syntax (group (fn () => "constant") xname);
 
-val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
+val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
 
 
 (* patterns *)