clarified language markup: added "delimited" property;
authorwenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 5582842ac3cfb89f6
parent 55827 8a881f83e206
child 55829 b7bdea5336dd
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/symbol_pos.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/Tools/rail.ML
src/Pure/pure_syn.ML
src/Tools/Code/code_thingol.ML
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -86,7 +86,9 @@
     1.4          then txt1 ^ ": " ^ txt2
     1.5          else txt1 ^ " : " ^ txt2;
     1.6        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.7 -      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
     1.8 +      val _ =  (* ML_Lex.read (!?) *)
     1.9 +        ML_Context.eval_source_in (SOME ctxt) false
    1.10 +          {delimited = false, text = ml (txt1, txt2), pos = Position.none};
    1.11        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.12      in
    1.13        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Sat Mar 01 19:55:01 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Mar 01 22:46:31 2014 +0100
     2.3 @@ -114,13 +114,13 @@
     2.4  setup -- "document antiquotation"
     2.5  {*
     2.6    Thy_Output.antiquotation @{binding ML_cartouche}
     2.7 -    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) =>
     2.8 +    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
     2.9        let
    2.10          val toks =
    2.11            ML_Lex.read Position.none "fn _ => (" @
    2.12 -          ML_Lex.read pos txt @
    2.13 +          ML_Lex.read_source source @
    2.14            ML_Lex.read Position.none ");";
    2.15 -        val _ = ML_Context.eval_in (SOME context) false pos toks;
    2.16 +        val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
    2.17        in "" end);
    2.18  *}
    2.19  
    2.20 @@ -177,19 +177,19 @@
    2.21  structure ML_Tactic:
    2.22  sig
    2.23    val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
    2.24 -  val ml_tactic: string * Position.T -> Proof.context -> tactic
    2.25 +  val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
    2.26  end =
    2.27  struct
    2.28    structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
    2.29  
    2.30    val set = Data.put;
    2.31  
    2.32 -  fun ml_tactic (txt, pos) ctxt =
    2.33 +  fun ml_tactic source ctxt =
    2.34      let
    2.35        val ctxt' = ctxt |> Context.proof_map
    2.36 -        (ML_Context.expression pos
    2.37 +        (ML_Context.expression (#pos source)
    2.38            "fun tactic (ctxt : Proof.context) : tactic"
    2.39 -          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read pos txt));
    2.40 +          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source));
    2.41      in Data.get ctxt' ctxt end;
    2.42  end;
    2.43  *}
     3.1 --- a/src/Pure/General/symbol_pos.ML	Sat Mar 01 19:55:01 2014 +0100
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Mar 01 22:46:31 2014 +0100
     3.3 @@ -37,6 +37,7 @@
     3.4    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     3.5      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
     3.6    type text = string
     3.7 +  type source = {delimited: bool, text: text, pos: Position.T}
     3.8    val implode: T list -> text
     3.9    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    3.10    val explode: text * Position.T -> T list
    3.11 @@ -232,6 +233,7 @@
    3.12  (* compact representation -- with Symbol.DEL padding *)
    3.13  
    3.14  type text = string;
    3.15 +type source = {delimited: bool, text: text, pos: Position.T}
    3.16  
    3.17  fun pad [] = []
    3.18    | pad [(s, _)] = [s]
     4.1 --- a/src/Pure/Isar/args.ML	Sat Mar 01 19:55:01 2014 +0100
     4.2 +++ b/src/Pure/Isar/args.ML	Sat Mar 01 22:46:31 2014 +0100
     4.3 @@ -30,9 +30,9 @@
     4.4    val mode: string -> bool parser
     4.5    val maybe: 'a parser -> 'a option parser
     4.6    val cartouche_inner_syntax: string parser
     4.7 -  val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
     4.8 +  val cartouche_source_position: Symbol_Pos.source parser
     4.9    val name_inner_syntax: string parser
    4.10 -  val name_source_position: (Symbol_Pos.text * Position.T) parser
    4.11 +  val name_source_position: Symbol_Pos.source parser
    4.12    val name: string parser
    4.13    val binding: binding parser
    4.14    val alt_name: string parser
     5.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 01 19:55:01 2014 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 01 22:46:31 2014 +0100
     5.3 @@ -35,8 +35,7 @@
     5.4      Context.generic -> (string * thm list) list * Context.generic
     5.5    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
     5.6    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     5.7 -  val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     5.8 -    theory -> theory
     5.9 +  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    5.10    val internal: (morphism -> attribute) -> src
    5.11    val add_del: attribute -> attribute -> attribute context_parser
    5.12    val thm_sel: Facts.interval list parser
    5.13 @@ -185,12 +184,12 @@
    5.14    add_attribute name
    5.15      (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
    5.16  
    5.17 -fun attribute_setup name (txt, pos) cmt =
    5.18 -  Context.theory_map (ML_Context.expression pos
    5.19 +fun attribute_setup name source cmt =
    5.20 +  Context.theory_map (ML_Context.expression (#pos source)
    5.21      "val (name, scan, comment): binding * attribute context_parser * string"
    5.22      "Context.map_theory (Attrib.setup name scan comment)"
    5.23      (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    5.24 -      ML_Lex.read pos txt @
    5.25 +      ML_Lex.read_source source @
    5.26        ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    5.27  
    5.28  
     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 01 19:55:01 2014 +0100
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 01 22:46:31 2014 +0100
     6.3 @@ -6,20 +6,20 @@
     6.4  
     6.5  signature ISAR_CMD =
     6.6  sig
     6.7 -  val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
     6.8 -  val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
     6.9 -  val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    6.10 -  val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
    6.11 -  val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    6.12 -  val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    6.13 -  val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    6.14 +  val global_setup: Symbol_Pos.source -> theory -> theory
    6.15 +  val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
    6.16 +  val parse_ast_translation: Symbol_Pos.source -> theory -> theory
    6.17 +  val parse_translation: Symbol_Pos.source -> theory -> theory
    6.18 +  val print_translation: Symbol_Pos.source -> theory -> theory
    6.19 +  val typed_print_translation: Symbol_Pos.source -> theory -> theory
    6.20 +  val print_ast_translation: Symbol_Pos.source -> theory -> theory
    6.21    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    6.22    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    6.23 -  val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    6.24 +  val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
    6.25    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    6.26    val declaration: {syntax: bool, pervasive: bool} ->
    6.27 -    Symbol_Pos.text * Position.T -> local_theory -> local_theory
    6.28 -  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
    6.29 +    Symbol_Pos.source -> local_theory -> local_theory
    6.30 +  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
    6.31      string list -> local_theory -> local_theory
    6.32    val hide_class: bool -> xstring list -> theory -> theory
    6.33    val hide_type: bool -> xstring list -> theory -> theory
    6.34 @@ -36,7 +36,7 @@
    6.35    val immediate_proof: Toplevel.transition -> Toplevel.transition
    6.36    val done_proof: Toplevel.transition -> Toplevel.transition
    6.37    val skip_proof: Toplevel.transition -> Toplevel.transition
    6.38 -  val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    6.39 +  val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    6.40    val diag_state: Proof.context -> Toplevel.state
    6.41    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    6.42    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    6.43 @@ -56,10 +56,10 @@
    6.44    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    6.45    val print_type: (string list * (string * string option)) ->
    6.46      Toplevel.transition -> Toplevel.transition
    6.47 -  val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    6.48 -  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
    6.49 +  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    6.50 +  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
    6.51      Toplevel.transition -> Toplevel.transition
    6.52 -  val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    6.53 +  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    6.54  end;
    6.55  
    6.56  structure Isar_Cmd: ISAR_CMD =
    6.57 @@ -70,50 +70,50 @@
    6.58  
    6.59  (* generic setup *)
    6.60  
    6.61 -fun global_setup (txt, pos) =
    6.62 -  ML_Lex.read pos txt
    6.63 -  |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
    6.64 +fun global_setup source =
    6.65 +  ML_Lex.read_source source
    6.66 +  |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
    6.67    |> Context.theory_map;
    6.68  
    6.69 -fun local_setup (txt, pos) =
    6.70 -  ML_Lex.read pos txt
    6.71 -  |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
    6.72 +fun local_setup source =
    6.73 +  ML_Lex.read_source source
    6.74 +  |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    6.75    |> Context.proof_map;
    6.76  
    6.77  
    6.78  (* translation functions *)
    6.79  
    6.80 -fun parse_ast_translation (txt, pos) =
    6.81 -  ML_Lex.read pos txt
    6.82 -  |> ML_Context.expression pos
    6.83 +fun parse_ast_translation source =
    6.84 +  ML_Lex.read_source source
    6.85 +  |> ML_Context.expression (#pos source)
    6.86      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    6.87      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    6.88    |> Context.theory_map;
    6.89  
    6.90 -fun parse_translation (txt, pos) =
    6.91 -  ML_Lex.read pos txt
    6.92 -  |> ML_Context.expression pos
    6.93 +fun parse_translation source =
    6.94 +  ML_Lex.read_source source
    6.95 +  |> ML_Context.expression (#pos source)
    6.96      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    6.97      "Context.map_theory (Sign.parse_translation parse_translation)"
    6.98    |> Context.theory_map;
    6.99  
   6.100 -fun print_translation (txt, pos) =
   6.101 -  ML_Lex.read pos txt
   6.102 -  |> ML_Context.expression pos
   6.103 +fun print_translation source =
   6.104 +  ML_Lex.read_source source
   6.105 +  |> ML_Context.expression (#pos source)
   6.106      "val print_translation: (string * (Proof.context -> term list -> term)) list"
   6.107      "Context.map_theory (Sign.print_translation print_translation)"
   6.108    |> Context.theory_map;
   6.109  
   6.110 -fun typed_print_translation (txt, pos) =
   6.111 -  ML_Lex.read pos txt
   6.112 -  |> ML_Context.expression pos
   6.113 +fun typed_print_translation source =
   6.114 +  ML_Lex.read_source source
   6.115 +  |> ML_Context.expression (#pos source)
   6.116      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
   6.117      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   6.118    |> Context.theory_map;
   6.119  
   6.120 -fun print_ast_translation (txt, pos) =
   6.121 -  ML_Lex.read pos txt
   6.122 -  |> ML_Context.expression pos
   6.123 +fun print_ast_translation source =
   6.124 +  ML_Lex.read_source source
   6.125 +  |> ML_Context.expression (#pos source)
   6.126      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   6.127      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   6.128    |> Context.theory_map;
   6.129 @@ -135,18 +135,19 @@
   6.130  
   6.131  (* oracles *)
   6.132  
   6.133 -fun oracle (name, pos) (body_txt, body_pos) =
   6.134 +fun oracle (name, pos) source =
   6.135    let
   6.136 -    val body = ML_Lex.read body_pos body_txt;
   6.137 +    val body = ML_Lex.read_source source;
   6.138      val ants =
   6.139        ML_Lex.read Position.none
   6.140         ("local\n\
   6.141          \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
   6.142          \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
   6.143          \in\n\
   6.144 -        \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
   6.145 +        \  val " ^ name ^
   6.146 +        " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
   6.147          \end;\n");
   6.148 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
   6.149 +  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
   6.150  
   6.151  
   6.152  (* old-style defs *)
   6.153 @@ -161,9 +162,9 @@
   6.154  
   6.155  (* declarations *)
   6.156  
   6.157 -fun declaration {syntax, pervasive} (txt, pos) =
   6.158 -  ML_Lex.read pos txt
   6.159 -  |> ML_Context.expression pos
   6.160 +fun declaration {syntax, pervasive} source =
   6.161 +  ML_Lex.read_source source
   6.162 +  |> ML_Context.expression (#pos source)
   6.163      "val declaration: Morphism.declaration"
   6.164      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   6.165        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   6.166 @@ -172,9 +173,9 @@
   6.167  
   6.168  (* simprocs *)
   6.169  
   6.170 -fun simproc_setup name lhss (txt, pos) identifier =
   6.171 -  ML_Lex.read pos txt
   6.172 -  |> ML_Context.expression pos
   6.173 +fun simproc_setup name lhss source identifier =
   6.174 +  ML_Lex.read_source source
   6.175 +  |> ML_Context.expression (#pos source)
   6.176      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
   6.177      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
   6.178        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   6.179 @@ -253,11 +254,11 @@
   6.180    fun init _ = Toplevel.toplevel;
   6.181  );
   6.182  
   6.183 -fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   6.184 +fun ml_diag verbose source = Toplevel.keep (fn state =>
   6.185    let val opt_ctxt =
   6.186      try Toplevel.generic_theory_of state
   6.187      |> Option.map (Context.proof_of #> Diag_State.put state)
   6.188 -  in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
   6.189 +  in ML_Context.eval_source_in opt_ctxt verbose source end);
   6.190  
   6.191  val diag_state = Diag_State.get;
   6.192  
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 01 19:55:01 2014 +0100
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 01 22:46:31 2014 +0100
     7.3 @@ -248,16 +248,17 @@
     7.4  
     7.5  val _ =
     7.6    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
     7.7 -    (Parse.ML_source >> (fn (txt, pos) =>
     7.8 +    (Parse.ML_source >> (fn source =>
     7.9        Toplevel.generic_theory
    7.10 -        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
    7.11 +        (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
    7.12            Local_Theory.propagate_ml_env)));
    7.13  
    7.14  val _ =
    7.15    Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
    7.16 -    (Parse.ML_source >> (fn (txt, pos) =>
    7.17 +    (Parse.ML_source >> (fn source =>
    7.18        Toplevel.proof (Proof.map_context (Context.proof_map
    7.19 -        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
    7.20 +        (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
    7.21 +          Proof.propagate_ml_env)));
    7.22  
    7.23  val _ =
    7.24    Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
     8.1 --- a/src/Pure/Isar/method.ML	Sat Mar 01 19:55:01 2014 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Sat Mar 01 22:46:31 2014 +0100
     8.3 @@ -42,8 +42,8 @@
     8.4    val drule: Proof.context -> int -> thm list -> method
     8.5    val frule: Proof.context -> int -> thm list -> method
     8.6    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
     8.7 -  val tactic: string * Position.T -> Proof.context -> method
     8.8 -  val raw_tactic: string * Position.T -> Proof.context -> method
     8.9 +  val tactic: Symbol_Pos.source -> Proof.context -> method
    8.10 +  val raw_tactic: Symbol_Pos.source -> Proof.context -> method
    8.11    type src = Args.src
    8.12    type combinator_info
    8.13    val no_combinator_info: combinator_info
    8.14 @@ -68,8 +68,7 @@
    8.15    val check_source: Proof.context -> src -> src
    8.16    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    8.17    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    8.18 -  val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    8.19 -    theory -> theory
    8.20 +  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    8.21    type modifier = (Proof.context -> Proof.context) * attribute
    8.22    val section: modifier parser list -> thm list context_parser
    8.23    val sections: modifier parser list -> thm list list context_parser
    8.24 @@ -266,16 +265,16 @@
    8.25  
    8.26  val set_tactic = ML_Tactic.put;
    8.27  
    8.28 -fun ml_tactic (txt, pos) ctxt =
    8.29 +fun ml_tactic source ctxt =
    8.30    let
    8.31      val ctxt' = ctxt |> Context.proof_map
    8.32 -      (ML_Context.expression pos
    8.33 +      (ML_Context.expression (#pos source)
    8.34          "fun tactic (facts: thm list) : tactic"
    8.35 -        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
    8.36 +        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source source));
    8.37    in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
    8.38  
    8.39 -fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    8.40 -fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
    8.41 +fun tactic source ctxt = METHOD (ml_tactic source ctxt);
    8.42 +fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt);
    8.43  
    8.44  
    8.45  
    8.46 @@ -366,12 +365,12 @@
    8.47    add_method name
    8.48      (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end);
    8.49  
    8.50 -fun method_setup name (txt, pos) cmt =
    8.51 -  Context.theory_map (ML_Context.expression pos
    8.52 +fun method_setup name source cmt =
    8.53 +  Context.theory_map (ML_Context.expression (#pos source)
    8.54      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    8.55      "Context.map_theory (Method.setup name scan comment)"
    8.56      (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    8.57 -      ML_Lex.read pos txt @
    8.58 +      ML_Lex.read_source source @
    8.59        ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    8.60  
    8.61  
     9.1 --- a/src/Pure/Isar/parse.ML	Sat Mar 01 19:55:01 2014 +0100
     9.2 +++ b/src/Pure/Isar/parse.ML	Sat Mar 01 22:46:31 2014 +0100
     9.3 @@ -16,7 +16,7 @@
     9.4    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
     9.5    val not_eof: Token.T parser
     9.6    val position: 'a parser -> ('a * Position.T) parser
     9.7 -  val source_position: 'a parser -> (Symbol_Pos.text * Position.T) parser
     9.8 +  val source_position: 'a parser -> Symbol_Pos.source parser
     9.9    val inner_syntax: 'a parser -> string parser
    9.10    val command: string parser
    9.11    val keyword: string parser
    9.12 @@ -93,8 +93,8 @@
    9.13    val simple_fixes: (binding * string option) list parser
    9.14    val fixes: (binding * string option * mixfix) list parser
    9.15    val for_fixes: (binding * string option * mixfix) list parser
    9.16 -  val ML_source: (Symbol_Pos.text * Position.T) parser
    9.17 -  val document_source: (Symbol_Pos.text * Position.T) parser
    9.18 +  val ML_source: Symbol_Pos.source parser
    9.19 +  val document_source: Symbol_Pos.source parser
    9.20    val term_group: string parser
    9.21    val prop_group: string parser
    9.22    val term: string parser
    10.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 01 19:55:01 2014 +0100
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 01 22:46:31 2014 +0100
    10.3 @@ -377,7 +377,8 @@
    10.4  fun read_class ctxt text =
    10.5    let
    10.6      val tsig = tsig_of ctxt;
    10.7 -    val (syms, pos) = Syntax.read_token text;
    10.8 +    val {text, pos, ...} = Syntax.read_token_source text;
    10.9 +    val syms = Symbol_Pos.explode (text, pos);
   10.10      val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
   10.11        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   10.12      val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   10.13 @@ -439,8 +440,6 @@
   10.14  
   10.15  local
   10.16  
   10.17 -val token_content = Syntax.read_token #>> Symbol_Pos.content;
   10.18 -
   10.19  fun prep_const_proper ctxt strict (c, pos) =
   10.20    let
   10.21      fun err msg = error (msg ^ Position.here pos);
   10.22 @@ -461,7 +460,7 @@
   10.23  fun read_type_name ctxt strict text =
   10.24    let
   10.25      val tsig = tsig_of ctxt;
   10.26 -    val (c, pos) = token_content text;
   10.27 +    val (c, pos) = Syntax.read_token_content text;
   10.28    in
   10.29      if Lexicon.is_tid c then
   10.30       (Context_Position.report ctxt pos Markup.tfree;
   10.31 @@ -486,11 +485,12 @@
   10.32    | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
   10.33  
   10.34  
   10.35 -fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
   10.36 +fun read_const_proper ctxt strict =
   10.37 +  prep_const_proper ctxt strict o Syntax.read_token_content;
   10.38  
   10.39  fun read_const ctxt strict ty text =
   10.40    let
   10.41 -    val (c, pos) = token_content text;
   10.42 +    val (c, pos) = Syntax.read_token_content text;
   10.43      val _ = no_skolem false c;
   10.44    in
   10.45      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    11.1 --- a/src/Pure/Isar/token.ML	Sat Mar 01 19:55:01 2014 +0100
    11.2 +++ b/src/Pure/Isar/token.ML	Sat Mar 01 22:46:31 2014 +0100
    11.3 @@ -40,7 +40,7 @@
    11.4    val is_blank: T -> bool
    11.5    val is_newline: T -> bool
    11.6    val inner_syntax_of: T -> string
    11.7 -  val source_position_of: T -> Symbol_Pos.text * Position.T
    11.8 +  val source_position_of: T -> Symbol_Pos.source
    11.9    val content_of: T -> string
   11.10    val markup: T -> Markup.T * string
   11.11    val unparse: T -> string
   11.12 @@ -127,6 +127,8 @@
   11.13    | Sync => "sync marker"
   11.14    | EOF => "end-of-input";
   11.15  
   11.16 +val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
   11.17 +
   11.18  
   11.19  (* position *)
   11.20  
   11.21 @@ -206,11 +208,16 @@
   11.22  
   11.23  (* token content *)
   11.24  
   11.25 -fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
   11.26 +fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) =
   11.27    if YXML.detect x then x
   11.28 -  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
   11.29 +  else
   11.30 +    let
   11.31 +      val delimited = delimited_kind kind;
   11.32 +      val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
   11.33 +    in YXML.string_of tree end;
   11.34  
   11.35 -fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
   11.36 +fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
   11.37 +  {delimited = delimited_kind kind, text = source, pos = pos};
   11.38  
   11.39  fun content_of (Token (_, (_, x), _)) = x;
   11.40  
    12.1 --- a/src/Pure/ML/ml_context.ML	Sat Mar 01 19:55:01 2014 +0100
    12.2 +++ b/src/Pure/ML/ml_context.ML	Sat Mar 01 22:46:31 2014 +0100
    12.3 @@ -31,10 +31,10 @@
    12.4    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    12.5      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
    12.6    val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
    12.7 -  val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit
    12.8 +  val eval_source: bool -> Symbol_Pos.source -> unit
    12.9    val eval_in: Proof.context option -> bool -> Position.T ->
   12.10      ML_Lex.token Antiquote.antiquote list -> unit
   12.11 -  val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
   12.12 +  val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
   12.13    val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
   12.14      Context.generic -> Context.generic
   12.15  end
   12.16 @@ -208,13 +208,14 @@
   12.17  
   12.18  (* derived versions *)
   12.19  
   12.20 -fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt);
   12.21 +fun eval_source verbose source =
   12.22 +  eval verbose (#pos source) (ML_Lex.read_source source);
   12.23  
   12.24  fun eval_in ctxt verbose pos ants =
   12.25    Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
   12.26  
   12.27 -fun eval_text_in ctxt verbose pos txt =
   12.28 -  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) ();
   12.29 +fun eval_source_in ctxt verbose source =
   12.30 +  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) ();
   12.31  
   12.32  fun expression pos bind body ants =
   12.33    exec (fn () => eval false pos
    13.1 --- a/src/Pure/ML/ml_lex.ML	Sat Mar 01 19:55:01 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Mar 01 22:46:31 2014 +0100
    13.3 @@ -26,6 +26,7 @@
    13.4        Source.source) Source.source
    13.5    val tokenize: string -> token list
    13.6    val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
    13.7 +  val read_source: Symbol_Pos.source -> token Antiquote.antiquote list
    13.8  end;
    13.9  
   13.10  structure ML_Lex: ML_LEX =
   13.11 @@ -298,10 +299,9 @@
   13.12  
   13.13  val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
   13.14  
   13.15 -fun read pos txt =
   13.16 +fun read pos text =
   13.17    let
   13.18 -    val _ = Position.report pos Markup.language_ML;
   13.19 -    val syms = Symbol_Pos.explode (txt, pos);
   13.20 +    val syms = Symbol_Pos.explode (text, pos);
   13.21      val termination =
   13.22        if null syms then []
   13.23        else
   13.24 @@ -318,6 +318,9 @@
   13.25          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
   13.26    in input @ termination end;
   13.27  
   13.28 +fun read_source {delimited, text, pos} =
   13.29 +  (Position.report pos (Markup.language_ML delimited); read pos text);
   13.30 +
   13.31  end;
   13.32  
   13.33  end;
    14.1 --- a/src/Pure/PIDE/markup.ML	Sat Mar 01 19:55:01 2014 +0100
    14.2 +++ b/src/Pure/PIDE/markup.ML	Sat Mar 01 22:46:31 2014 +0100
    14.3 @@ -20,18 +20,21 @@
    14.4    val name: string -> T -> T
    14.5    val kindN: string
    14.6    val instanceN: string
    14.7 +  val languageN: string
    14.8    val symbolsN: string
    14.9 -  val languageN: string
   14.10 -  val language: {name: string, symbols: bool, antiquotes: bool} -> T
   14.11 +  val delimitedN: string
   14.12 +  val is_delimited: Properties.T -> bool
   14.13 +  val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   14.14 +  val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   14.15    val language_method: T
   14.16 -  val language_sort: T
   14.17 -  val language_type: T
   14.18 -  val language_term: T
   14.19 -  val language_prop: T
   14.20 -  val language_ML: T
   14.21 -  val language_document: T
   14.22 +  val language_sort: bool -> T
   14.23 +  val language_type: bool -> T
   14.24 +  val language_term: bool -> T
   14.25 +  val language_prop: bool -> T
   14.26 +  val language_ML: bool -> T
   14.27 +  val language_document: bool -> T
   14.28    val language_antiquotation: T
   14.29 -  val language_text: T
   14.30 +  val language_text: bool -> T
   14.31    val language_rail: T
   14.32    val bindingN: string val binding: T
   14.33    val entityN: string val entity: string -> string -> T
   14.34 @@ -106,7 +109,7 @@
   14.35    val cartoucheN: string val cartouche: T
   14.36    val commentN: string val comment: T
   14.37    val controlN: string val control: T
   14.38 -  val tokenN: string val token: Properties.T -> T
   14.39 +  val tokenN: string val token: bool -> Properties.T -> T
   14.40    val keyword1N: string val keyword1: T
   14.41    val keyword2N: string val keyword2: T
   14.42    val keyword3N: string val keyword3: T
   14.43 @@ -251,24 +254,36 @@
   14.44  
   14.45  (* embedded languages *)
   14.46  
   14.47 +val languageN = "language";
   14.48  val symbolsN = "symbols";
   14.49  val antiquotesN = "antiquotes";
   14.50 -val languageN = "language";
   14.51 +val delimitedN = "delimited"
   14.52 +
   14.53 +fun is_delimited props =
   14.54 +  Properties.get props delimitedN = SOME "true";
   14.55  
   14.56 -fun language {name, symbols, antiquotes} =
   14.57 +fun language {name, symbols, antiquotes, delimited} =
   14.58    (languageN,
   14.59 -    [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
   14.60 +   [(nameN, name),
   14.61 +    (symbolsN, print_bool symbols),
   14.62 +    (antiquotesN, print_bool antiquotes),
   14.63 +    (delimitedN, print_bool delimited)]);
   14.64  
   14.65 -val language_method = language {name = "method", symbols = true, antiquotes = false};
   14.66 -val language_sort = language {name = "sort", symbols = true, antiquotes = false};
   14.67 -val language_type = language {name = "type", symbols = true, antiquotes = false};
   14.68 -val language_term = language {name = "term", symbols = true, antiquotes = false};
   14.69 -val language_prop = language {name = "prop", symbols = true, antiquotes = false};
   14.70 -val language_ML = language {name = "ML", symbols = false, antiquotes = true};
   14.71 -val language_document = language {name = "document", symbols = false, antiquotes = true};
   14.72 -val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false};
   14.73 -val language_text = language {name = "text", symbols = true, antiquotes = false};
   14.74 -val language_rail = language {name = "rail", symbols = true, antiquotes = true};
   14.75 +fun language' {name, symbols, antiquotes} delimited =
   14.76 +  language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
   14.77 +
   14.78 +val language_method =
   14.79 +  language {name = "method", symbols = true, antiquotes = false, delimited = false};
   14.80 +val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
   14.81 +val language_type = language' {name = "type", symbols = true, antiquotes = false};
   14.82 +val language_term = language' {name = "term", symbols = true, antiquotes = false};
   14.83 +val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
   14.84 +val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
   14.85 +val language_document = language' {name = "document", symbols = false, antiquotes = true};
   14.86 +val language_antiquotation =
   14.87 +  language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
   14.88 +val language_text = language' {name = "text", symbols = true, antiquotes = false};
   14.89 +val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
   14.90  
   14.91  
   14.92  (* formal entities *)
   14.93 @@ -411,7 +426,7 @@
   14.94  val (controlN, control) = markup_elem "control";
   14.95  
   14.96  val tokenN = "token";
   14.97 -fun token props = (tokenN, props);
   14.98 +fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);
   14.99  
  14.100  
  14.101  (* timing *)
    15.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 01 19:55:01 2014 +0100
    15.2 +++ b/src/Pure/PIDE/markup.scala	Sat Mar 01 22:46:31 2014 +0100
    15.3 @@ -94,6 +94,7 @@
    15.4  
    15.5    val Symbols = new Properties.Boolean("symbols")
    15.6    val Antiquotes = new Properties.Boolean("antiquotes")
    15.7 +  val Delimited = new Properties.Boolean("delimited")
    15.8  
    15.9    val LANGUAGE = "language"
   15.10    object Language
   15.11 @@ -101,12 +102,12 @@
   15.12      val ML = "ML"
   15.13      val UNKNOWN = "unknown"
   15.14  
   15.15 -    def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
   15.16 +    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
   15.17        markup match {
   15.18          case Markup(LANGUAGE, props) =>
   15.19 -          (props, props, props) match {
   15.20 -            case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
   15.21 -              Some((name, symbols, antiquotes))
   15.22 +          (props, props, props, props) match {
   15.23 +            case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
   15.24 +              Some((name, symbols, antiquotes, delimited))
   15.25              case _ => None
   15.26            }
   15.27          case _ => None
    16.1 --- a/src/Pure/Syntax/syntax.ML	Sat Mar 01 19:55:01 2014 +0100
    16.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Mar 01 22:46:31 2014 +0100
    16.3 @@ -14,10 +14,11 @@
    16.4    val ambiguity_warning: bool Config.T
    16.5    val ambiguity_limit_raw: Config.raw
    16.6    val ambiguity_limit: int Config.T
    16.7 -  val read_token: string -> Symbol_Pos.T list * Position.T
    16.8    val read_token_pos: string -> Position.T
    16.9 +  val read_token_source: string -> Symbol_Pos.source
   16.10 +  val read_token_content: string -> string * Position.T
   16.11    val parse_token: Proof.context -> (XML.tree list -> 'a) ->
   16.12 -    Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   16.13 +    (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   16.14    val parse_sort: Proof.context -> string -> sort
   16.15    val parse_typ: Proof.context -> string -> typ
   16.16    val parse_term: Proof.context -> string -> term
   16.17 @@ -159,26 +160,39 @@
   16.18  
   16.19  (* outer syntax token -- with optional YXML content *)
   16.20  
   16.21 +local
   16.22 +
   16.23  fun token_position (XML.Elem ((name, props), _)) =
   16.24 -      if name = Markup.tokenN then Position.of_properties props
   16.25 -      else Position.none
   16.26 -  | token_position (XML.Text _) = Position.none;
   16.27 +      if name = Markup.tokenN
   16.28 +      then (Markup.is_delimited props, Position.of_properties props)
   16.29 +      else (false, Position.none)
   16.30 +  | token_position (XML.Text _) = (false, Position.none);
   16.31  
   16.32 -fun explode_token tree =
   16.33 +fun token_source tree =
   16.34    let
   16.35      val text = XML.content_of [tree];
   16.36 -    val pos = token_position tree;
   16.37 -  in (Symbol_Pos.explode (text, pos), pos) end;
   16.38 +    val (delimited, pos) = token_position tree;
   16.39 +  in {delimited = delimited, text = text, pos = pos} end;
   16.40 +
   16.41 +in
   16.42 +
   16.43 +fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
   16.44  
   16.45 -fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
   16.46 -fun read_token_pos str = token_position (YXML.parse str handle Fail msg => error msg);
   16.47 +fun read_token_source str = token_source (YXML.parse str handle Fail msg => error msg);
   16.48 +
   16.49 +fun read_token_content str =
   16.50 +  let
   16.51 +    val {text, pos, ...} = read_token_source str;
   16.52 +    val syms = Symbol_Pos.explode (text, pos);
   16.53 +  in (Symbol_Pos.content syms, pos) end;
   16.54  
   16.55  fun parse_token ctxt decode markup parse str =
   16.56    let
   16.57      fun parse_tree tree =
   16.58        let
   16.59 -        val (syms, pos) = explode_token tree;
   16.60 -        val _ = Context_Position.report ctxt pos markup;
   16.61 +        val {delimited, text, pos} = token_source tree;
   16.62 +        val syms = Symbol_Pos.explode (text, pos);
   16.63 +        val _ = Context_Position.report ctxt pos (markup delimited);
   16.64        in parse (syms, pos) end;
   16.65    in
   16.66      (case YXML.parse_body str handle Fail msg => error msg of
   16.67 @@ -188,6 +202,8 @@
   16.68      | body => decode body)
   16.69    end;
   16.70  
   16.71 +end;
   16.72 +
   16.73  
   16.74  (* (un)parsing *)
   16.75  
    17.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 19:55:01 2014 +0100
    17.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 22:46:31 2014 +0100
    17.3 @@ -440,7 +440,8 @@
    17.4            else decode_appl ps asts
    17.5        | decode ps (Ast.Appl asts) = decode_appl ps asts;
    17.6  
    17.7 -    val (syms, pos) = Syntax.read_token str;
    17.8 +    val {text, pos, ...} = Syntax.read_token_source str;
    17.9 +    val syms = Symbol_Pos.explode (text, pos);
   17.10      val ast =
   17.11        parse_asts ctxt true root (syms, pos)
   17.12        |> uncurry (report_result ctxt pos)
   17.13 @@ -749,8 +750,8 @@
   17.14  
   17.15  in
   17.16  
   17.17 -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
   17.18 -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
   17.19 +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
   17.20 +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
   17.21  
   17.22  fun unparse_term ctxt =
   17.23    let
   17.24 @@ -760,7 +761,7 @@
   17.25    in
   17.26      unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
   17.27        (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
   17.28 -      Markup.language_term ctxt
   17.29 +      (Markup.language_term false) ctxt
   17.30    end;
   17.31  
   17.32  end;
    18.1 --- a/src/Pure/Thy/latex.ML	Sat Mar 01 19:55:01 2014 +0100
    18.2 +++ b/src/Pure/Thy/latex.ML	Sat Mar 01 22:46:31 2014 +0100
    18.3 @@ -121,8 +121,8 @@
    18.4        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    18.5      else if Token.is_kind Token.Verbatim tok then
    18.6        let
    18.7 -        val (txt, pos) = Token.source_position_of tok;
    18.8 -        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    18.9 +        val {text, pos, ...} = Token.source_position_of tok;
   18.10 +        val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
   18.11          val out = implode (map output_syms_antiq ants);
   18.12        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   18.13      else if Token.is_kind Token.Cartouche tok then
    19.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 01 19:55:01 2014 +0100
    19.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Mar 01 22:46:31 2014 +0100
    19.3 @@ -25,7 +25,7 @@
    19.4    datatype markup = Markup | MarkupEnv | Verbatim
    19.5    val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
    19.6    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
    19.7 -  val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
    19.8 +  val check_text: Symbol_Pos.source -> Toplevel.state -> unit
    19.9    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
   19.10      (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   19.11    val pretty_text: Proof.context -> string -> Pretty.T
   19.12 @@ -184,10 +184,10 @@
   19.13    end;
   19.14  
   19.15  
   19.16 -fun check_text (txt, pos) state =
   19.17 - (Position.report pos Markup.language_document;
   19.18 +fun check_text {delimited, text, pos} state =
   19.19 + (Position.report pos (Markup.language_document delimited);
   19.20    if Toplevel.is_skipped_proof state then ()
   19.21 -  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
   19.22 +  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos)));
   19.23  
   19.24  
   19.25  
   19.26 @@ -360,9 +360,9 @@
   19.27          Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
   19.28        Scan.repeat tag --
   19.29        Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
   19.30 -      >> (fn (((tok, pos), tags), txt) =>
   19.31 +      >> (fn (((tok, pos'), tags), {text, pos, ...}) =>
   19.32          let val name = Token.content_of tok
   19.33 -        in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
   19.34 +        in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
   19.35  
   19.36      val command = Scan.peek (fn d =>
   19.37        Parse.position (Scan.one (Token.is_command)) --
   19.38 @@ -373,7 +373,7 @@
   19.39  
   19.40      val cmt = Scan.peek (fn d =>
   19.41        Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
   19.42 -      >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
   19.43 +      >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
   19.44  
   19.45      val other = Scan.peek (fn d =>
   19.46         Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
   19.47 @@ -467,8 +467,11 @@
   19.48  fun pretty_text ctxt =
   19.49    Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
   19.50  
   19.51 -fun pretty_text_report ctxt (s, pos) =
   19.52 -  (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s);
   19.53 +fun pretty_text_report ctxt {delimited, text, pos} =
   19.54 +  let
   19.55 +    val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
   19.56 +    val s = Symbol_Pos.content (Symbol_Pos.explode (text, pos));
   19.57 +  in pretty_text ctxt s end;
   19.58  
   19.59  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
   19.60  
   19.61 @@ -574,7 +577,7 @@
   19.62    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   19.63    basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
   19.64    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   19.65 -  basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #>
   19.66 +  basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #>
   19.67    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
   19.68    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
   19.69    basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
   19.70 @@ -638,15 +641,17 @@
   19.71  local
   19.72  
   19.73  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   19.74 -  (fn {context, ...} => fn (txt, pos) =>
   19.75 -   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
   19.76 -    Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
   19.77 +  (fn {context, ...} => fn source as {text, pos, ...} =>
   19.78 +   (ML_Context.eval_in (SOME context) false pos (ml source);
   19.79 +    Symbol_Pos.content (Symbol_Pos.explode (text, pos))
   19.80      |> (if Config.get context quotes then quote else I)
   19.81      |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   19.82          else verb_text)));
   19.83  
   19.84 -fun ml_enclose bg en pos txt =
   19.85 -  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
   19.86 +fun ml_enclose bg en source =
   19.87 +  ML_Lex.read Position.none bg @
   19.88 +  ML_Lex.read_source source @
   19.89 +  ML_Lex.read Position.none en;
   19.90  
   19.91  in
   19.92  
   19.93 @@ -658,11 +663,11 @@
   19.94      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
   19.95  
   19.96    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
   19.97 -    (fn pos => fn txt =>
   19.98 +    (fn {text, pos, ...} =>
   19.99        ML_Lex.read Position.none ("ML_Env.check_functor " ^
  19.100 -        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
  19.101 +        ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (text, pos))))) #>
  19.102  
  19.103 -  ml_text (Binding.name "ML_text") (K (K [])));
  19.104 +  ml_text (Binding.name "ML_text") (K []));
  19.105  
  19.106  end;
  19.107  
    20.1 --- a/src/Pure/Thy/thy_syntax.ML	Sat Mar 01 19:55:01 2014 +0100
    20.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sat Mar 01 22:46:31 2014 +0100
    20.3 @@ -44,14 +44,15 @@
    20.4  
    20.5  fun reports_of_token tok =
    20.6    let
    20.7 +    val {text, pos, ...} = Token.source_position_of tok;
    20.8      val malformed_symbols =
    20.9 -      Symbol_Pos.explode (Token.source_position_of tok)
   20.10 +      Symbol_Pos.explode (text, pos)
   20.11        |> map_filter (fn (sym, pos) =>
   20.12            if Symbol.is_malformed sym
   20.13            then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
   20.14      val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
   20.15 -    val (markup, txt) = Token.markup tok;
   20.16 -    val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols;
   20.17 +    val (markup, msg) = Token.markup tok;
   20.18 +    val reports = ((Token.pos_of tok, markup), msg) :: malformed_symbols;
   20.19    in (is_malformed, reports) end;
   20.20  
   20.21  in
    21.1 --- a/src/Pure/Tools/rail.ML	Sat Mar 01 19:55:01 2014 +0100
    21.2 +++ b/src/Pure/Tools/rail.ML	Sat Mar 01 22:46:31 2014 +0100
    21.3 @@ -192,10 +192,11 @@
    21.4  
    21.5  in
    21.6  
    21.7 -fun read ctxt (s, pos) =
    21.8 +fun read ctxt (source: Symbol_Pos.source) =
    21.9    let
   21.10 +    val {text, pos, ...} = source;
   21.11      val _ = Context_Position.report ctxt pos Markup.language_rail;
   21.12 -    val toks = tokenize (Symbol_Pos.explode (s, pos));
   21.13 +    val toks = tokenize (Symbol_Pos.explode (text, pos));
   21.14      val _ = Context_Position.reports ctxt (maps reports_of_token toks);
   21.15    in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
   21.16  
    22.1 --- a/src/Pure/pure_syn.ML	Sat Mar 01 19:55:01 2014 +0100
    22.2 +++ b/src/Pure/pure_syn.ML	Sat Mar 01 22:46:31 2014 +0100
    22.3 @@ -24,9 +24,10 @@
    22.4          let
    22.5            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    22.6            val provide = Thy_Load.provide (src_path, digest);
    22.7 +          val source = {delimited = true, text = cat_lines lines, pos = pos};
    22.8          in
    22.9            gthy
   22.10 -          |> ML_Context.exec (fn () => ML_Context.eval_text true pos (cat_lines lines))
   22.11 +          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
   22.12            |> Local_Theory.propagate_ml_env
   22.13            |> Context.mapping provide (Local_Theory.background_theory provide)
   22.14          end)));
    23.1 --- a/src/Tools/Code/code_thingol.ML	Sat Mar 01 19:55:01 2014 +0100
    23.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Mar 01 22:46:31 2014 +0100
    23.3 @@ -882,7 +882,7 @@
    23.4        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
    23.5      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
    23.6      fun read_const_expr str =
    23.7 -      (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
    23.8 +      (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
    23.9          SOME "_" => ([], consts_of thy)
   23.10        | SOME s =>
   23.11            if String.isSuffix "._" s
    24.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 19:55:01 2014 +0100
    24.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Mar 01 22:46:31 2014 +0100
    24.3 @@ -150,7 +150,7 @@
    24.4            val context =
    24.5              (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    24.6                case Some(rendering) =>
    24.7 -                rendering.language_context(before_caret_range(rendering))
    24.8 +                rendering.completion_language(before_caret_range(rendering))
    24.9                case None => None
   24.10              }) getOrElse syntax.language_context
   24.11  
    25.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 19:55:01 2014 +0100
    25.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 22:46:31 2014 +0100
    25.3 @@ -132,7 +132,7 @@
    25.4    private val completion_names_elements =
    25.5      Document.Elements(Markup.COMPLETION)
    25.6  
    25.7 -  private val language_context_elements =
    25.8 +  private val completion_language_elements =
    25.9      Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   25.10        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
   25.11        Markup.ML_STRING, Markup.ML_COMMENT)
   25.12 @@ -267,11 +267,12 @@
   25.13          }).headOption.map(_.info)
   25.14      }
   25.15  
   25.16 -  def language_context(range: Text.Range): Option[Completion.Language_Context] =
   25.17 -    snapshot.select(range, Rendering.language_context_elements, _ =>
   25.18 +  def completion_language(range: Text.Range): Option[Completion.Language_Context] =
   25.19 +    snapshot.select(range, Rendering.completion_language_elements, _ =>
   25.20        {
   25.21 -        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
   25.22 -          Some(Completion.Language_Context(language, symbols, antiquotes))
   25.23 +        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
   25.24 +          if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
   25.25 +          else None
   25.26          case Text.Info(_, elem)
   25.27          if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
   25.28            Some(Completion.Language_Context.ML_inner)
   25.29 @@ -485,7 +486,7 @@
   25.30              Some(add(prev, r, (true, pretty_typing("::", body))))
   25.31            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   25.32              Some(add(prev, r, (false, pretty_typing("ML:", body))))
   25.33 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _), _))) =>
   25.34 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   25.35              Some(add(prev, r, (true, XML.Text("language: " + language))))
   25.36            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   25.37              Rendering.tooltip_descriptions.get(name).