# HG changeset patch
# User wenzelm
# Date 1409233646 -7200
# Node ID 0255436b3d859b74db55b8582ce4a01b56795a28
# Parent  d6f29bf9b783067e5b82df402be393cbab9e0b05
more liberal embedded "text", which includes cartouches;

diff -r d6f29bf9b783 -r 0255436b3d85 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 28 13:25:12 2014 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 28 15:47:26 2014 +0200
@@ -166,18 +166,18 @@
       @@{antiquotation typ} options @{syntax type} |
       @@{antiquotation type} options @{syntax name} |
       @@{antiquotation class} options @{syntax name} |
-      @@{antiquotation text} options @{syntax name}
+      @@{antiquotation text} options @{syntax text}
     ;
     @{syntax antiquotation}:
       @@{antiquotation goals} options |
       @@{antiquotation subgoals} options |
       @@{antiquotation prf} options @{syntax thmrefs} |
       @@{antiquotation full_prf} options @{syntax thmrefs} |
-      @@{antiquotation ML} options @{syntax name} |
-      @@{antiquotation ML_op} options @{syntax name} |
-      @@{antiquotation ML_type} options @{syntax name} |
-      @@{antiquotation ML_structure} options @{syntax name} |
-      @@{antiquotation ML_functor} options @{syntax name} |
+      @@{antiquotation ML} options @{syntax text} |
+      @@{antiquotation ML_op} options @{syntax text} |
+      @@{antiquotation ML_type} options @{syntax text} |
+      @@{antiquotation ML_structure} options @{syntax text} |
+      @@{antiquotation ML_functor} options @{syntax text} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name}
diff -r d6f29bf9b783 -r 0255436b3d85 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Thu Aug 28 13:25:12 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Thu Aug 28 15:47:26 2014 +0200
@@ -81,7 +81,7 @@
   (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
-  (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position)))
+  (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
   (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
     let
       val (txt1, toks1) = prep_ml source1;
diff -r d6f29bf9b783 -r 0255436b3d85 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Aug 28 13:25:12 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Aug 28 15:47:26 2014 +0200
@@ -583,7 +583,7 @@
   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.name_source_position) pretty_text_report #>
+  basic_entity @{binding text} (Scan.lift Args.text_source_position) 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);
@@ -645,7 +645,7 @@
 
 local
 
-fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
+fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
   (fn {context, ...} => fn source =>
    (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
     Symbol_Pos.source_content source