1.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 28 13:25:12 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 28 15:47:26 2014 +0200
     1.3 @@ -166,18 +166,18 @@
     1.4        @@{antiquotation typ} options @{syntax type} |
     1.5        @@{antiquotation type} options @{syntax name} |
     1.6        @@{antiquotation class} options @{syntax name} |
     1.7 -      @@{antiquotation text} options @{syntax name}
     1.8 +      @@{antiquotation text} options @{syntax text}
     1.9      ;
    1.10      @{syntax antiquotation}:
    1.11        @@{antiquotation goals} options |
    1.12        @@{antiquotation subgoals} options |
    1.13        @@{antiquotation prf} options @{syntax thmrefs} |
    1.14        @@{antiquotation full_prf} options @{syntax thmrefs} |
    1.15 -      @@{antiquotation ML} options @{syntax name} |
    1.16 -      @@{antiquotation ML_op} options @{syntax name} |
    1.17 -      @@{antiquotation ML_type} options @{syntax name} |
    1.18 -      @@{antiquotation ML_structure} options @{syntax name} |
    1.19 -      @@{antiquotation ML_functor} options @{syntax name} |
    1.20 +      @@{antiquotation ML} options @{syntax text} |
    1.21 +      @@{antiquotation ML_op} options @{syntax text} |
    1.22 +      @@{antiquotation ML_type} options @{syntax text} |
    1.23 +      @@{antiquotation ML_structure} options @{syntax text} |
    1.24 +      @@{antiquotation ML_functor} options @{syntax text} |
    1.25        @@{antiquotation "file"} options @{syntax name} |
    1.26        @@{antiquotation file_unchecked} options @{syntax name} |
    1.27        @@{antiquotation url} options @{syntax name}

     2.1 --- a/src/Doc/antiquote_setup.ML	Thu Aug 28 13:25:12 2014 +0200
     2.2 +++ b/src/Doc/antiquote_setup.ML	Thu Aug 28 15:47:26 2014 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4    (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
     2.5  
     2.6  fun index_ml name kind ml = Thy_Output.antiquotation name
     2.7 -  (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position)))
     2.8 +  (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
     2.9    (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
    2.10      let
    2.11        val (txt1, toks1) = prep_ml source1;

     3.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 28 13:25:12 2014 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Aug 28 15:47:26 2014 +0200
     3.3 @@ -583,7 +583,7 @@
     3.4    basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
     3.5    basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
     3.6    basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
     3.7 -  basic_entity @{binding text} (Scan.lift Args.name_source_position) pretty_text_report #>
     3.8 +  basic_entity @{binding text} (Scan.lift Args.text_source_position) pretty_text_report #>
     3.9    basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
    3.10    basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
    3.11    basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
    3.12 @@ -645,7 +645,7 @@
    3.13  
    3.14  local
    3.15  
    3.16 -fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    3.17 +fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
    3.18    (fn {context, ...} => fn source =>
    3.19     (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
    3.20      Symbol_Pos.source_content source