src/Pure/ML/ml_antiquotations.ML
changeset 67146 909dcdec2122
parent 64594 4719f13989df
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  val _ = Theory.setup
     1.6   (ML_Antiquotation.value @{binding system_option}
     1.7 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
     1.8 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
     1.9        let
    1.10          val markup =
    1.11            Options.default_markup (name, pos) handle ERROR msg =>
    1.12 @@ -57,13 +57,13 @@
    1.13        in ML_Syntax.print_string name end)) #>
    1.14  
    1.15    ML_Antiquotation.value @{binding theory}
    1.16 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    1.17 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    1.18        (Theory.check ctxt (name, pos);
    1.19         "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    1.20      || Scan.succeed "Proof_Context.theory_of ML_context") #>
    1.21  
    1.22    ML_Antiquotation.value @{binding theory_context}
    1.23 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    1.24 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    1.25        (Theory.check ctxt (name, pos);
    1.26         "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    1.27          ML_Syntax.print_string name))) #>
    1.28 @@ -85,7 +85,7 @@
    1.29      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    1.30  
    1.31    ML_Antiquotation.inline @{binding method}
    1.32 -    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    1.33 +    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    1.34        ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
    1.35  
    1.36  
    1.37 @@ -93,7 +93,7 @@
    1.38  
    1.39  val _ = Theory.setup
    1.40   (ML_Antiquotation.inline @{binding locale}
    1.41 -   (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    1.42 +   (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
    1.43        Locale.check (Proof_Context.theory_of ctxt) (name, pos)
    1.44        |> ML_Syntax.print_string)));
    1.45  
    1.46 @@ -260,14 +260,14 @@
    1.47  
    1.48  val _ = Theory.setup
    1.49   (ML_Antiquotation.value @{binding keyword}
    1.50 -    (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
    1.51 +    (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true)))
    1.52        >> (fn (ctxt, (name, pos)) =>
    1.53          if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
    1.54            (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
    1.55             "Parse.$$$ " ^ ML_Syntax.print_string name)
    1.56          else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
    1.57    ML_Antiquotation.value @{binding command_keyword}
    1.58 -    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
    1.59 +    (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) =>
    1.60        (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
    1.61          SOME markup =>
    1.62           (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];