--- 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}
--- 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;
--- 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