# HG changeset patch # User wenzelm # Date 1393710391 -3600 # Node ID 42ac3cfb89f6582d80ddb849eaa3e08903f76b1a # Parent 8a881f83e206c68f5a96584ea71c62c1b3135fe8 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"; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Sat Mar 01 22:46:31 2014 +0100 @@ -86,7 +86,9 @@ then txt1 ^ ": " ^ txt2 else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; - val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) + val _ = (* ML_Lex.read (!?) *) + ML_Context.eval_source_in (SOME ctxt) false + {delimited = false, text = ml (txt1, txt2), pos = Position.none}; val kind' = if kind = "" then "ML" else "ML " ^ kind; in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ diff -r 8a881f83e206 -r 42ac3cfb89f6 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Sat Mar 01 19:55:01 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Sat Mar 01 22:46:31 2014 +0100 @@ -114,13 +114,13 @@ setup -- "document antiquotation" {* Thy_Output.antiquotation @{binding ML_cartouche} - (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) => + (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source => let val toks = ML_Lex.read Position.none "fn _ => (" @ - ML_Lex.read pos txt @ + ML_Lex.read_source source @ ML_Lex.read Position.none ");"; - val _ = ML_Context.eval_in (SOME context) false pos toks; + val _ = ML_Context.eval_in (SOME context) false (#pos source) toks; in "" end); *} @@ -177,19 +177,19 @@ structure ML_Tactic: sig val set: (Proof.context -> tactic) -> Proof.context -> Proof.context - val ml_tactic: string * Position.T -> Proof.context -> tactic + val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic end = struct structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac); val set = Data.put; - fun ml_tactic (txt, pos) ctxt = + fun ml_tactic source ctxt = let val ctxt' = ctxt |> Context.proof_map - (ML_Context.expression pos + (ML_Context.expression (#pos source) "fun tactic (ctxt : Proof.context) : tactic" - "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read pos txt)); + "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source)); in Data.get ctxt' ctxt end; end; *} diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Sat Mar 01 22:46:31 2014 +0100 @@ -37,6 +37,7 @@ val source: Position.T -> (Symbol.symbol, 'a) Source.source -> (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source type text = string + type source = {delimited: bool, text: text, pos: Position.T} val implode: T list -> text val implode_range: Position.T -> Position.T -> T list -> text * Position.range val explode: text * Position.T -> T list @@ -232,6 +233,7 @@ (* compact representation -- with Symbol.DEL padding *) type text = string; +type source = {delimited: bool, text: text, pos: Position.T} fun pad [] = [] | pad [(s, _)] = [s] diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/args.ML Sat Mar 01 22:46:31 2014 +0100 @@ -30,9 +30,9 @@ val mode: string -> bool parser val maybe: 'a parser -> 'a option parser val cartouche_inner_syntax: string parser - val cartouche_source_position: (Symbol_Pos.text * Position.T) parser + val cartouche_source_position: Symbol_Pos.source parser val name_inner_syntax: string parser - val name_source_position: (Symbol_Pos.text * Position.T) parser + val name_source_position: Symbol_Pos.source parser val name: string parser val binding: binding parser val alt_name: string parser diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Mar 01 22:46:31 2014 +0100 @@ -35,8 +35,7 @@ Context.generic -> (string * thm list) list * Context.generic val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory - val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> - theory -> theory + val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory val internal: (morphism -> attribute) -> src val add_del: attribute -> attribute -> attribute context_parser val thm_sel: Facts.interval list parser @@ -185,12 +184,12 @@ add_attribute name (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end); -fun attribute_setup name (txt, pos) cmt = - Context.theory_map (ML_Context.expression pos +fun attribute_setup name source cmt = + Context.theory_map (ML_Context.expression (#pos source) "val (name, scan, comment): binding * attribute context_parser * string" "Context.map_theory (Attrib.setup name scan comment)" (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read pos txt @ + ML_Lex.read_source source @ ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))); diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Mar 01 22:46:31 2014 +0100 @@ -6,20 +6,20 @@ signature ISAR_CMD = sig - val global_setup: Symbol_Pos.text * Position.T -> theory -> theory - val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context - val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory - val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory - val print_translation: Symbol_Pos.text * Position.T -> theory -> theory - val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory - val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory + val global_setup: Symbol_Pos.source -> theory -> theory + val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context + val parse_ast_translation: Symbol_Pos.source -> theory -> theory + val parse_translation: Symbol_Pos.source -> theory -> theory + val print_translation: Symbol_Pos.source -> theory -> theory + val typed_print_translation: Symbol_Pos.source -> theory -> theory + val print_ast_translation: Symbol_Pos.source -> theory -> theory val translations: (xstring * string) Syntax.trrule list -> theory -> theory val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory - val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory + val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> - Symbol_Pos.text * Position.T -> local_theory -> local_theory - val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T -> + Symbol_Pos.source -> local_theory -> local_theory + val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source -> string list -> local_theory -> local_theory val hide_class: bool -> xstring list -> theory -> theory val hide_type: bool -> xstring list -> theory -> theory @@ -36,7 +36,7 @@ val immediate_proof: Toplevel.transition -> Toplevel.transition val done_proof: Toplevel.transition -> Toplevel.transition val skip_proof: Toplevel.transition -> Toplevel.transition - val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition + val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition val diag_state: Proof.context -> Toplevel.state val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm} val print_theorems: bool -> Toplevel.transition -> Toplevel.transition @@ -56,10 +56,10 @@ val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition val print_type: (string list * (string * string option)) -> Toplevel.transition -> Toplevel.transition - val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition - val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) -> + val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition + val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) -> Toplevel.transition -> Toplevel.transition - val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition + val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition end; structure Isar_Cmd: ISAR_CMD = @@ -70,50 +70,50 @@ (* generic setup *) -fun global_setup (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" +fun global_setup source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup" |> Context.theory_map; -fun local_setup (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup" +fun local_setup source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup" |> Context.proof_map; (* translation functions *) -fun parse_ast_translation (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun parse_ast_translation source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)" |> Context.theory_map; -fun parse_translation (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun parse_translation source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val parse_translation: (string * (Proof.context -> term list -> term)) list" "Context.map_theory (Sign.parse_translation parse_translation)" |> Context.theory_map; -fun print_translation (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun print_translation source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val print_translation: (string * (Proof.context -> term list -> term)) list" "Context.map_theory (Sign.print_translation print_translation)" |> Context.theory_map; -fun typed_print_translation (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun typed_print_translation source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list" "Context.map_theory (Sign.typed_print_translation typed_print_translation)" |> Context.theory_map; -fun print_ast_translation (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun print_ast_translation source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" "Context.map_theory (Sign.print_ast_translation print_ast_translation)" |> Context.theory_map; @@ -135,18 +135,19 @@ (* oracles *) -fun oracle (name, pos) (body_txt, body_pos) = +fun oracle (name, pos) source = let - val body = ML_Lex.read body_pos body_txt; + val body = ML_Lex.read_source source; val ants = ML_Lex.read Position.none ("local\n\ \ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\ \ val body = ") @ body @ ML_Lex.read Position.none (";\n\ \in\n\ - \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\ + \ val " ^ name ^ + " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\ \end;\n"); - in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end; + in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end; (* old-style defs *) @@ -161,9 +162,9 @@ (* declarations *) -fun declaration {syntax, pervasive} (txt, pos) = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun declaration {syntax, pervasive} source = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val declaration: Morphism.declaration" ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \ \pervasive = " ^ Bool.toString pervasive ^ "} declaration)") @@ -172,9 +173,9 @@ (* simprocs *) -fun simproc_setup name lhss (txt, pos) identifier = - ML_Lex.read pos txt - |> ML_Context.expression pos +fun simproc_setup name lhss source identifier = + ML_Lex.read_source source + |> ML_Context.expression (#pos source) "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option" ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ @@ -253,11 +254,11 @@ fun init _ = Toplevel.toplevel; ); -fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => +fun ml_diag verbose source = Toplevel.keep (fn state => let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put state) - in ML_Context.eval_text_in opt_ctxt verbose pos txt end); + in ML_Context.eval_source_in opt_ctxt verbose source end); val diag_state = Diag_State.get; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sat Mar 01 22:46:31 2014 +0100 @@ -248,16 +248,17 @@ val _ = Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory" - (Parse.ML_source >> (fn (txt, pos) => + (Parse.ML_source >> (fn source => Toplevel.generic_theory - (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> + (ML_Context.exec (fn () => ML_Context.eval_source true source) #> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof" - (Parse.ML_source >> (fn (txt, pos) => + (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map - (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env))); + (ML_Context.exec (fn () => ML_Context.eval_source true source))) #> + Proof.propagate_ml_env))); val _ = Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text" diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/method.ML Sat Mar 01 22:46:31 2014 +0100 @@ -42,8 +42,8 @@ val drule: Proof.context -> int -> thm list -> method val frule: Proof.context -> int -> thm list -> method val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context - val tactic: string * Position.T -> Proof.context -> method - val raw_tactic: string * Position.T -> Proof.context -> method + val tactic: Symbol_Pos.source -> Proof.context -> method + val raw_tactic: Symbol_Pos.source -> Proof.context -> method type src = Args.src type combinator_info val no_combinator_info: combinator_info @@ -68,8 +68,7 @@ val check_source: Proof.context -> src -> src val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory - val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> - theory -> theory + val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory type modifier = (Proof.context -> Proof.context) * attribute val section: modifier parser list -> thm list context_parser val sections: modifier parser list -> thm list list context_parser @@ -266,16 +265,16 @@ val set_tactic = ML_Tactic.put; -fun ml_tactic (txt, pos) ctxt = +fun ml_tactic source ctxt = let val ctxt' = ctxt |> Context.proof_map - (ML_Context.expression pos + (ML_Context.expression (#pos source) "fun tactic (facts: thm list) : tactic" - "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt)); + "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source source)); in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end; -fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); -fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); +fun tactic source ctxt = METHOD (ml_tactic source ctxt); +fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt); @@ -366,12 +365,12 @@ add_method name (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end); -fun method_setup name (txt, pos) cmt = - Context.theory_map (ML_Context.expression pos +fun method_setup name source cmt = + Context.theory_map (ML_Context.expression (#pos source) "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" "Context.map_theory (Method.setup name scan comment)" (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read pos txt @ + ML_Lex.read_source source @ ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))); diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/parse.ML Sat Mar 01 22:46:31 2014 +0100 @@ -16,7 +16,7 @@ val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b val not_eof: Token.T parser val position: 'a parser -> ('a * Position.T) parser - val source_position: 'a parser -> (Symbol_Pos.text * Position.T) parser + val source_position: 'a parser -> Symbol_Pos.source parser val inner_syntax: 'a parser -> string parser val command: string parser val keyword: string parser @@ -93,8 +93,8 @@ val simple_fixes: (binding * string option) list parser val fixes: (binding * string option * mixfix) list parser val for_fixes: (binding * string option * mixfix) list parser - val ML_source: (Symbol_Pos.text * Position.T) parser - val document_source: (Symbol_Pos.text * Position.T) parser + val ML_source: Symbol_Pos.source parser + val document_source: Symbol_Pos.source parser val term_group: string parser val prop_group: string parser val term: string parser diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 01 22:46:31 2014 +0100 @@ -377,7 +377,8 @@ fun read_class ctxt text = let val tsig = tsig_of ctxt; - val (syms, pos) = Syntax.read_token text; + val {text, pos, ...} = Syntax.read_token_source text; + val syms = Symbol_Pos.explode (text, pos); val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms)) handle TYPE (msg, _, _) => error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c); @@ -439,8 +440,6 @@ local -val token_content = Syntax.read_token #>> Symbol_Pos.content; - fun prep_const_proper ctxt strict (c, pos) = let fun err msg = error (msg ^ Position.here pos); @@ -461,7 +460,7 @@ fun read_type_name ctxt strict text = let val tsig = tsig_of ctxt; - val (c, pos) = token_content text; + val (c, pos) = Syntax.read_token_content text; in if Lexicon.is_tid c then (Context_Position.report ctxt pos Markup.tfree; @@ -486,11 +485,12 @@ | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T)); -fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content; +fun read_const_proper ctxt strict = + prep_const_proper ctxt strict o Syntax.read_token_content; fun read_const ctxt strict ty text = let - val (c, pos) = token_content text; + val (c, pos) = Syntax.read_token_content text; val _ = no_skolem false c; in (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Isar/token.ML Sat Mar 01 22:46:31 2014 +0100 @@ -40,7 +40,7 @@ val is_blank: T -> bool val is_newline: T -> bool val inner_syntax_of: T -> string - val source_position_of: T -> Symbol_Pos.text * Position.T + val source_position_of: T -> Symbol_Pos.source val content_of: T -> string val markup: T -> Markup.T * string val unparse: T -> string @@ -127,6 +127,8 @@ | Sync => "sync marker" | EOF => "end-of-input"; +val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment]; + (* position *) @@ -206,11 +208,16 @@ (* token content *) -fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) = +fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) = if YXML.detect x then x - else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source])); + else + let + val delimited = delimited_kind kind; + val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]); + in YXML.string_of tree end; -fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos); +fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) = + {delimited = delimited_kind kind, text = source, pos = pos}; fun content_of (Token (_, (_, x), _)) = x; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Sat Mar 01 22:46:31 2014 +0100 @@ -31,10 +31,10 @@ val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit - val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit + val eval_source: bool -> Symbol_Pos.source -> unit val eval_in: Proof.context option -> bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit - val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit + val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic end @@ -208,13 +208,14 @@ (* derived versions *) -fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt); +fun eval_source verbose source = + eval verbose (#pos source) (ML_Lex.read_source source); fun eval_in ctxt verbose pos ants = Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) (); -fun eval_text_in ctxt verbose pos txt = - Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) (); +fun eval_source_in ctxt verbose source = + Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) (); fun expression pos bind body ants = exec (fn () => eval false pos diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Sat Mar 01 22:46:31 2014 +0100 @@ -26,6 +26,7 @@ Source.source) Source.source val tokenize: string -> token list val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list + val read_source: Symbol_Pos.source -> token Antiquote.antiquote list end; structure ML_Lex: ML_LEX = @@ -298,10 +299,9 @@ val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust; -fun read pos txt = +fun read pos text = let - val _ = Position.report pos Markup.language_ML; - val syms = Symbol_Pos.explode (txt, pos); + val syms = Symbol_Pos.explode (text, pos); val termination = if null syms then [] else @@ -318,6 +318,9 @@ |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))); in input @ termination end; +fun read_source {delimited, text, pos} = + (Position.report pos (Markup.language_ML delimited); read pos text); + end; end; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Mar 01 22:46:31 2014 +0100 @@ -20,18 +20,21 @@ val name: string -> T -> T val kindN: string val instanceN: string + val languageN: string val symbolsN: string - val languageN: string - val language: {name: string, symbols: bool, antiquotes: bool} -> T + val delimitedN: string + val is_delimited: Properties.T -> bool + val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T + val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_method: T - val language_sort: T - val language_type: T - val language_term: T - val language_prop: T - val language_ML: T - val language_document: T + val language_sort: bool -> T + val language_type: bool -> T + val language_term: bool -> T + val language_prop: bool -> T + val language_ML: bool -> T + val language_document: bool -> T val language_antiquotation: T - val language_text: T + val language_text: bool -> T val language_rail: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T @@ -106,7 +109,7 @@ val cartoucheN: string val cartouche: T val commentN: string val comment: T val controlN: string val control: T - val tokenN: string val token: Properties.T -> T + val tokenN: string val token: bool -> Properties.T -> T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T val keyword3N: string val keyword3: T @@ -251,24 +254,36 @@ (* embedded languages *) +val languageN = "language"; val symbolsN = "symbols"; val antiquotesN = "antiquotes"; -val languageN = "language"; +val delimitedN = "delimited" + +fun is_delimited props = + Properties.get props delimitedN = SOME "true"; -fun language {name, symbols, antiquotes} = +fun language {name, symbols, antiquotes, delimited} = (languageN, - [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]); + [(nameN, name), + (symbolsN, print_bool symbols), + (antiquotesN, print_bool antiquotes), + (delimitedN, print_bool delimited)]); -val language_method = language {name = "method", symbols = true, antiquotes = false}; -val language_sort = language {name = "sort", symbols = true, antiquotes = false}; -val language_type = language {name = "type", symbols = true, antiquotes = false}; -val language_term = language {name = "term", symbols = true, antiquotes = false}; -val language_prop = language {name = "prop", symbols = true, antiquotes = false}; -val language_ML = language {name = "ML", symbols = false, antiquotes = true}; -val language_document = language {name = "document", symbols = false, antiquotes = true}; -val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false}; -val language_text = language {name = "text", symbols = true, antiquotes = false}; -val language_rail = language {name = "rail", symbols = true, antiquotes = true}; +fun language' {name, symbols, antiquotes} delimited = + language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; + +val language_method = + language {name = "method", symbols = true, antiquotes = false, delimited = false}; +val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; +val language_type = language' {name = "type", symbols = true, antiquotes = false}; +val language_term = language' {name = "term", symbols = true, antiquotes = false}; +val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; +val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; +val language_document = language' {name = "document", symbols = false, antiquotes = true}; +val language_antiquotation = + language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; +val language_text = language' {name = "text", symbols = true, antiquotes = false}; +val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; (* formal entities *) @@ -411,7 +426,7 @@ val (controlN, control) = markup_elem "control"; val tokenN = "token"; -fun token props = (tokenN, props); +fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props); (* timing *) diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Sat Mar 01 22:46:31 2014 +0100 @@ -94,6 +94,7 @@ val Symbols = new Properties.Boolean("symbols") val Antiquotes = new Properties.Boolean("antiquotes") + val Delimited = new Properties.Boolean("delimited") val LANGUAGE = "language" object Language @@ -101,12 +102,12 @@ val ML = "ML" val UNKNOWN = "unknown" - def unapply(markup: Markup): Option[(String, Boolean, Boolean)] = + def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] = markup match { case Markup(LANGUAGE, props) => - (props, props, props) match { - case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) => - Some((name, symbols, antiquotes)) + (props, props, props, props) match { + case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => + Some((name, symbols, antiquotes, delimited)) case _ => None } case _ => None diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Syntax/syntax.ML Sat Mar 01 22:46:31 2014 +0100 @@ -14,10 +14,11 @@ val ambiguity_warning: bool Config.T val ambiguity_limit_raw: Config.raw val ambiguity_limit: int Config.T - val read_token: string -> Symbol_Pos.T list * Position.T val read_token_pos: string -> Position.T + val read_token_source: string -> Symbol_Pos.source + val read_token_content: string -> string * Position.T val parse_token: Proof.context -> (XML.tree list -> 'a) -> - Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a + (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ val parse_term: Proof.context -> string -> term @@ -159,26 +160,39 @@ (* outer syntax token -- with optional YXML content *) +local + fun token_position (XML.Elem ((name, props), _)) = - if name = Markup.tokenN then Position.of_properties props - else Position.none - | token_position (XML.Text _) = Position.none; + if name = Markup.tokenN + then (Markup.is_delimited props, Position.of_properties props) + else (false, Position.none) + | token_position (XML.Text _) = (false, Position.none); -fun explode_token tree = +fun token_source tree = let val text = XML.content_of [tree]; - val pos = token_position tree; - in (Symbol_Pos.explode (text, pos), pos) end; + val (delimited, pos) = token_position tree; + in {delimited = delimited, text = text, pos = pos} end; + +in + +fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg)); -fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg); -fun read_token_pos str = token_position (YXML.parse str handle Fail msg => error msg); +fun read_token_source str = token_source (YXML.parse str handle Fail msg => error msg); + +fun read_token_content str = + let + val {text, pos, ...} = read_token_source str; + val syms = Symbol_Pos.explode (text, pos); + in (Symbol_Pos.content syms, pos) end; fun parse_token ctxt decode markup parse str = let fun parse_tree tree = let - val (syms, pos) = explode_token tree; - val _ = Context_Position.report ctxt pos markup; + val {delimited, text, pos} = token_source tree; + val syms = Symbol_Pos.explode (text, pos); + val _ = Context_Position.report ctxt pos (markup delimited); in parse (syms, pos) end; in (case YXML.parse_body str handle Fail msg => error msg of @@ -188,6 +202,8 @@ | body => decode body) end; +end; + (* (un)parsing *) diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 22:46:31 2014 +0100 @@ -440,7 +440,8 @@ else decode_appl ps asts | decode ps (Ast.Appl asts) = decode_appl ps asts; - val (syms, pos) = Syntax.read_token str; + val {text, pos, ...} = Syntax.read_token_source str; + val syms = Symbol_Pos.explode (text, pos); val ast = parse_asts ctxt true root (syms, pos) |> uncurry (report_result ctxt pos) @@ -749,8 +750,8 @@ in -val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort; -val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type; +val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false); +val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false); fun unparse_term ctxt = let @@ -760,7 +761,7 @@ in unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn)) (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) - Markup.language_term ctxt + (Markup.language_term false) ctxt end; end; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Thy/latex.ML Sat Mar 01 22:46:31 2014 +0100 @@ -121,8 +121,8 @@ enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) else if Token.is_kind Token.Verbatim tok then let - val (txt, pos) = Token.source_position_of tok; - val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); + val {text, pos, ...} = Token.source_position_of tok; + val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos); val out = implode (map output_syms_antiq ants); in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end else if Token.is_kind Token.Cartouche tok then diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Mar 01 22:46:31 2014 +0100 @@ -25,7 +25,7 @@ datatype markup = Markup | MarkupEnv | Verbatim val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string - val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit + val check_text: Symbol_Pos.source -> Toplevel.state -> unit val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T val pretty_text: Proof.context -> string -> Pretty.T @@ -184,10 +184,10 @@ end; -fun check_text (txt, pos) state = - (Position.report pos Markup.language_document; +fun check_text {delimited, text, pos} state = + (Position.report pos (Markup.language_document delimited); if Toplevel.is_skipped_proof state then () - else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); + else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos))); @@ -360,9 +360,9 @@ Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) -- Scan.repeat tag -- Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end) - >> (fn (((tok, pos), tags), txt) => + >> (fn (((tok, pos'), tags), {text, pos, ...}) => let val name = Token.content_of tok - in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end)); + in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end)); val command = Scan.peek (fn d => Parse.position (Scan.one (Token.is_command)) -- @@ -373,7 +373,7 @@ val cmt = Scan.peek (fn d => Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) - >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d))))); + >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d))))); val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d))))); @@ -467,8 +467,11 @@ fun pretty_text ctxt = Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines; -fun pretty_text_report ctxt (s, pos) = - (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s); +fun pretty_text_report ctxt {delimited, text, pos} = + let + val _ = Context_Position.report ctxt pos (Markup.language_text delimited); + val s = Symbol_Pos.content (Symbol_Pos.explode (text, pos)); + in pretty_text ctxt s end; fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; @@ -574,7 +577,7 @@ basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #> basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #> basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #> - basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #> + basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #> basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #> basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #> basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory); @@ -638,15 +641,17 @@ local fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position) - (fn {context, ...} => fn (txt, pos) => - (ML_Context.eval_in (SOME context) false pos (ml pos txt); - Symbol_Pos.content (Symbol_Pos.explode (txt, pos)) + (fn {context, ...} => fn source as {text, pos, ...} => + (ML_Context.eval_in (SOME context) false pos (ml source); + Symbol_Pos.content (Symbol_Pos.explode (text, pos)) |> (if Config.get context quotes then quote else I) |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" else verb_text))); -fun ml_enclose bg en pos txt = - ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en; +fun ml_enclose bg en source = + ML_Lex.read Position.none bg @ + ML_Lex.read_source source @ + ML_Lex.read Position.none en; in @@ -658,11 +663,11 @@ (ml_enclose "functor XXX() = struct structure XX = " " end;") #> ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *) - (fn pos => fn txt => + (fn {text, pos, ...} => ML_Lex.read Position.none ("ML_Env.check_functor " ^ - ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #> + ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (text, pos))))) #> - ml_text (Binding.name "ML_text") (K (K []))); + ml_text (Binding.name "ML_text") (K [])); end; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Sat Mar 01 22:46:31 2014 +0100 @@ -44,14 +44,15 @@ fun reports_of_token tok = let + val {text, pos, ...} = Token.source_position_of tok; val malformed_symbols = - Symbol_Pos.explode (Token.source_position_of tok) + Symbol_Pos.explode (text, pos) |> map_filter (fn (sym, pos) => if Symbol.is_malformed sym then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE); val is_malformed = Token.is_error tok orelse not (null malformed_symbols); - val (markup, txt) = Token.markup tok; - val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols; + val (markup, msg) = Token.markup tok; + val reports = ((Token.pos_of tok, markup), msg) :: malformed_symbols; in (is_malformed, reports) end; in diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/Tools/rail.ML Sat Mar 01 22:46:31 2014 +0100 @@ -192,10 +192,11 @@ in -fun read ctxt (s, pos) = +fun read ctxt (source: Symbol_Pos.source) = let + val {text, pos, ...} = source; val _ = Context_Position.report ctxt pos Markup.language_rail; - val toks = tokenize (Symbol_Pos.explode (s, pos)); + val toks = tokenize (Symbol_Pos.explode (text, pos)); val _ = Context_Position.reports ctxt (maps reports_of_token toks); in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end; diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Pure/pure_syn.ML Sat Mar 01 22:46:31 2014 +0100 @@ -24,9 +24,10 @@ let val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); val provide = Thy_Load.provide (src_path, digest); + val source = {delimited = true, text = cat_lines lines, pos = pos}; in gthy - |> ML_Context.exec (fn () => ML_Context.eval_text true pos (cat_lines lines)) + |> ML_Context.exec (fn () => ML_Context.eval_source true source) |> Local_Theory.propagate_ml_env |> Context.mapping provide (Local_Theory.background_theory provide) end))); diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Sat Mar 01 22:46:31 2014 +0100 @@ -882,7 +882,7 @@ (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); fun read_const_expr str = - (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of + (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of SOME "_" => ([], consts_of thy) | SOME s => if String.isSuffix "._" s diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Sat Mar 01 22:46:31 2014 +0100 @@ -150,7 +150,7 @@ val context = (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match { case Some(rendering) => - rendering.language_context(before_caret_range(rendering)) + rendering.completion_language(before_caret_range(rendering)) case None => None }) getOrElse syntax.language_context diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Mar 01 19:55:01 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 01 22:46:31 2014 +0100 @@ -132,7 +132,7 @@ private val completion_names_elements = Document.Elements(Markup.COMPLETION) - private val language_context_elements = + private val completion_language_elements = Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT) @@ -267,11 +267,12 @@ }).headOption.map(_.info) } - def language_context(range: Text.Range): Option[Completion.Language_Context] = - snapshot.select(range, Rendering.language_context_elements, _ => + def completion_language(range: Text.Range): Option[Completion.Language_Context] = + snapshot.select(range, Rendering.completion_language_elements, _ => { - case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) => - Some(Completion.Language_Context(language, symbols, antiquotes)) + case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => + if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) + else None case Text.Info(_, elem) if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => Some(Completion.Language_Context.ML_inner) @@ -485,7 +486,7 @@ Some(add(prev, r, (true, pretty_typing("::", body)))) case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(add(prev, r, (false, pretty_typing("ML:", body)))) - case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _), _))) => + case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) => Some(add(prev, r, (true, XML.Text("language: " + language)))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => Rendering.tooltip_descriptions.get(name).