# HG changeset patch # User wenzelm # Date 1418074932 -3600 # Node ID e670969f34dfc4d47e7c14a8132f44fd0b82c6a3 # Parent c85e018be3a3f3a850523138e7806294cdefe06e expand ML cartouches to Input.source; tuned signature; diff -r c85e018be3a3 -r e670969f34df NEWS --- a/NEWS Mon Dec 08 16:04:50 2014 +0100 +++ b/NEWS Mon Dec 08 22:42:12 2014 +0100 @@ -218,6 +218,9 @@ *** ML *** +* Cartouches within ML sources are turned into values of type +Input.source (with formal position information). + * Proper context for various elementary tactics: assume_tac, match_tac, compose_tac, Splitter.split_tac etc. Minor INCOMPATIBILITY. diff -r c85e018be3a3 -r e670969f34df src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Mon Dec 08 16:04:50 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Mon Dec 08 22:42:12 2014 +0100 @@ -260,4 +260,15 @@ lemma "A \ B \ B \ A" by (\rtac @{thm impI} 1\, \etac @{thm conjE} 1\, \rtac @{thm conjI} 1\, \atac 1\+) + +subsection \ML syntax: input source\ + +ML \ + val s: Input.source = \abc\; + writeln ("Look here!" ^ Position.here (Input.pos_of s)); + + \abc123def456\ |> Input.source_explode |> List.app (fn (s, pos) => + if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ()); +\ + end diff -r c85e018be3a3 -r e670969f34df src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/General/antiquote.ML Mon Dec 08 22:42:12 2014 +0100 @@ -8,7 +8,6 @@ sig type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} datatype 'a antiquote = Text of 'a | Antiq of antiq - val is_text: 'a antiquote -> bool val antiq_reports: antiq -> Position.report list val antiquote_reports: ('a -> Position.report_text list) -> 'a antiquote list -> Position.report_text list @@ -25,9 +24,6 @@ type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; datatype 'a antiquote = Text of 'a | Antiq of antiq; -fun is_text (Text _) = true - | is_text _ = false; - (* reports *) diff -r c85e018be3a3 -r e670969f34df src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Mon Dec 08 22:42:12 2014 +0100 @@ -37,7 +37,7 @@ (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source type text = string val implode: T list -> text - val implode_range: Position.T -> Position.T -> T list -> text * Position.range + val implode_range: Position.range -> T list -> text * Position.range val explode: text * Position.T -> T list val scan_ident: T list -> T list * T list val is_identifier: string -> bool @@ -238,7 +238,7 @@ val implode = implode o pad; -fun implode_range pos1 pos2 syms = +fun implode_range (pos1, pos2) syms = let val syms' = (("", pos1) :: syms @ [("", pos2)]) in (implode syms', range syms') end; diff -r c85e018be3a3 -r e670969f34df src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/Isar/token.ML Mon Dec 08 22:42:12 2014 +0100 @@ -542,7 +542,7 @@ Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = - Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot); + Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_antiquotation.ML Mon Dec 08 22:42:12 2014 +0100 @@ -6,7 +6,6 @@ signature ML_ANTIQUOTATION = sig - val variant: string -> Proof.context -> string * Proof.context val declaration: binding -> 'a context_parser -> (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> theory -> theory @@ -17,24 +16,6 @@ structure ML_Antiquotation: ML_ANTIQUOTATION = struct -(* unique names *) - -val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"]; - -structure Names = Proof_Data -( - type T = Name.context; - fun init _ = init_context; -); - -fun variant a ctxt = - let - val names = Names.get ctxt; - val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; - val ctxt' = Names.put names' ctxt; - in (b, ctxt') end; - - (* define antiquotations *) fun declaration name scan body = @@ -47,25 +28,15 @@ declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); fun value name scan = - declaration name scan (fn _ => fn s => fn ctxt => - let - val (a, ctxt') = variant (Binding.name_of name) ctxt; - val env = "val " ^ a ^ " = " ^ s ^ ";\n"; - val body = "Isabelle." ^ a; - in (K (env, body), ctxt') end); + declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name)); (* basic antiquotations *) val _ = Theory.setup (declaration (Binding.make ("here", @{here})) (Scan.succeed ()) - (fn src => fn () => fn ctxt => - let - val (a, ctxt') = variant "position" ctxt; - val (_, pos) = Token.name_of_src src; - val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; - val body = "Isabelle." ^ a; - in (K (env, body), ctxt') end) #> + (fn src => fn () => + ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> value (Binding.make ("binding", @{here})) (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding)); diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Mon Dec 08 22:42:12 2014 +0100 @@ -20,7 +20,7 @@ (fn src => fn output => fn ctxt => let val (_, pos) = Token.name_of_src src; - val (a, ctxt') = ML_Antiquotation.variant "output" ctxt; + val (a, ctxt') = ML_Context.variant "output" ctxt; val env = "val " ^ a ^ ": string -> unit =\n\ \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ @@ -30,16 +30,6 @@ in (K (env, body), ctxt') end)); -(* embedded source *) - -val _ = Theory.setup - (ML_Antiquotation.value @{binding source} - (Scan.lift Args.text_source_position >> (fn source => - "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^ - ML_Syntax.print_string (Input.text_of source) ^ " " ^ - ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))); - - (* formal entities *) val _ = Theory.setup diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Mon Dec 08 22:42:12 2014 +0100 @@ -13,7 +13,9 @@ val thms: xstring -> thm list val exec: (unit -> unit) -> Context.generic -> Context.generic val check_antiquotation: Proof.context -> xstring * Position.T -> string + val variant: string -> Proof.context -> string * Proof.context type decl = Proof.context -> string * string + val value_decl: string -> string -> Proof.context -> decl * Proof.context val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) -> theory -> theory val print_antiquotations: Proof.context -> unit @@ -50,9 +52,38 @@ (** ML antiquotations **) +(* unique names *) + +structure Names = Proof_Data +( + type T = Name.context; + val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"]; + fun init _ = init_names; +); + +fun variant a ctxt = + let + val names = Names.get ctxt; + val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; + val ctxt' = Names.put names' ctxt; + in (b, ctxt') end; + + +(* decl *) + +type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) + +fun value_decl a s ctxt = + let + val (b, ctxt') = variant a ctxt; + val env = "val " ^ b ^ " = " ^ s ^ ";\n"; + val body = "Isabelle." ^ b; + fun decl (_: Proof.context) = (env, body); + in (decl, ctxt') end; + + (* theory data *) -type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) structure Antiquotations = Theory_Data ( type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table; @@ -101,6 +132,9 @@ val end_env = ML_Lex.tokenize "end;"; val reset_env = ML_Lex.tokenize "structure Isabelle = struct end"; +fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok + | expanding (Antiquote.Antiq _) = true; + in fun eval_antiquotes (ants, pos) opt_context = @@ -112,20 +146,32 @@ val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context; val ((ml_env, ml_body), opt_ctxt') = - if forall Antiquote.is_text ants + if forall (not o expanding) ants then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt) else let - fun no_decl _ = ([], []); + fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); - fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) - | expand (Antiquote.Antiq (ss, {range, ...})) ctxt = + fun expand (Antiquote.Antiq (ss, {range, ...})) ctxt = let val keywords = Thy_Header.get_keywords' ctxt; val (decl, ctxt') = apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt; - val decl' = decl #> apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); - in (decl', ctxt') end; + in (decl #> tokenize range, ctxt') end + | expand (Antiquote.Text tok) ctxt = + if ML_Lex.is_cartouche tok then + let + val range = ML_Lex.range_of tok; + val text = + Symbol_Pos.explode (ML_Lex.content_of tok, #1 range) + |> Symbol_Pos.cartouche_content + |> Symbol_Pos.implode_range range |> #1; + val (decl, ctxt') = + value_decl "input" + ("Input.source true " ^ ML_Syntax.print_string text ^ " " ^ + ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt; + in (decl #> tokenize range, ctxt') end + else (K ([], [tok]), ctxt); val ctxt = (case opt_ctxt of diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Mon Dec 08 22:42:12 2014 +0100 @@ -9,12 +9,14 @@ val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF + Space | Cartouche | Comment | Error of string | EOF eqtype token val stopper: token Scan.stopper + val is_cartouche: token -> bool val is_regular: token -> bool val is_improper: token -> bool val set_range: Position.range -> token -> token + val range_of: token -> Position.range val pos_of: token -> Position.T val end_pos_of: token -> Position.T val kind_of: token -> token_kind @@ -62,7 +64,7 @@ datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF; + Space | Cartouche | Comment | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); @@ -70,9 +72,10 @@ (* position *) fun set_range range (Token (_, x)) = Token (range, x); +fun range_of (Token (range, _)) = range; -fun pos_of (Token ((pos, _), _)) = pos; -fun end_pos_of (Token ((_, pos), _)) = pos; +val pos_of = #1 o range_of; +val end_pos_of = #2 o range_of; (* stopper *) @@ -100,6 +103,9 @@ fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; +fun is_cartouche (Token (_, (Cartouche, _))) = true + | is_cartouche _ = false; + fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; @@ -121,6 +127,9 @@ Error msg => error msg | _ => content_of tok); + +(* flatten *) + fun flatten_content (tok :: (toks as tok' :: _)) = Symbol.escape (check_content_of tok) :: (if is_improper tok orelse is_improper tok' then flatten_content toks @@ -145,6 +154,7 @@ | Char => (Markup.ML_char, "") | String => (if SML then Markup.SML_string else Markup.ML_string, "") | Space => (Markup.empty, "") + | Cartouche => (Markup.ML_cartouche, "") | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "") | Error msg => (Markup.bad, msg) | EOF => (Markup.empty, ""); @@ -284,11 +294,17 @@ scan_ident >> token Ident || scan_type_var >> token Type_Var)); -val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text; +val scan_sml = scan_ml >> Antiquote.Text; + +val scan_ml_antiq = + Antiquote.scan_antiq >> Antiquote.Antiq || + Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) || + scan_ml >> Antiquote.Text; fun recover msg = (recover_char || recover_string || + Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); @@ -307,7 +323,7 @@ val pos2 = Position.advance Symbol.space pos1; in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end; - val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq; + val scan = if SML then scan_sml else scan_ml_antiq; fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok) | check _ = (); val input = diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_lex.scala Mon Dec 08 22:42:12 2014 +0100 @@ -50,6 +50,7 @@ val CHAR = Value("character") val STRING = Value("quoted string") val SPACE = Value("white space") + val CARTOUCHE = Value("text cartouche") val COMMENT = Value("comment text") val ANTIQ = Value("antiquotation") val ANTIQ_START = Value("antiquotation: start") @@ -133,6 +134,15 @@ } + /* ML cartouche */ + + private val ml_cartouche: Parser[Token] = + cartouche ^^ (x => Token(Kind.CARTOUCHE, x)) + + private def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.CARTOUCHE, x), c) } + + /* ML comment */ private val ml_comment: Parser[Token] = @@ -145,10 +155,11 @@ /* delimited token */ private def delimited_token: Parser[Token] = - ml_char | (ml_string | ml_comment) + ml_char | (ml_string | (ml_cartouche | ml_comment)) private val recover_delimited: Parser[Token] = - (recover_ml_char | (recover_ml_string | recover_comment)) ^^ (x => Token(Kind.ERROR, x)) + (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^ + (x => Token(Kind.ERROR, x)) private def other_token: Parser[Token] = @@ -246,8 +257,9 @@ if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other) else ml_string_line(ctxt) | - (ml_comment_line(ctxt) | - (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))) + (ml_cartouche_line(ctxt) | + (ml_comment_line(ctxt) | + (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))) } } diff -r c85e018be3a3 -r e670969f34df src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Mon Dec 08 22:42:12 2014 +0100 @@ -42,16 +42,12 @@ val _ = Theory.setup (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs) (fn _ => fn raw_srcs => fn ctxt => - let - val i = serial (); - - val (a, ctxt') = ctxt - |> ML_Antiquotation.variant "attributes" - ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs); - val ml = - ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ - string_of_int i ^ ";\n", "Isabelle." ^ a); - in (K ml, ctxt') end)); + let val i = serial () in + ctxt + |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs) + |> ML_Context.value_decl "attributes" + ("ML_Thms.the_attributes ML_context " ^ string_of_int i) + end)); (* fact references *) @@ -59,7 +55,7 @@ fun thm_binding kind is_single thms ctxt = let val initial = null (get_thmss ctxt); - val (name, ctxt') = ML_Antiquotation.variant kind ctxt; + val (name, ctxt') = ML_Context.variant kind ctxt; val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; val ml_body = "Isabelle." ^ name; diff -r c85e018be3a3 -r e670969f34df src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Dec 08 22:42:12 2014 +0100 @@ -99,6 +99,7 @@ val ML_numeralN: string val ML_numeral: T val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T + val ML_cartoucheN: string val ML_cartouche: T val ML_commentN: string val ML_comment: T val SML_stringN: string val SML_string: T val SML_commentN: string val SML_comment: T @@ -427,6 +428,7 @@ val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; +val (ML_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; val (SML_stringN, SML_string) = markup_elem "SML_string"; val (SML_commentN, SML_comment) = markup_elem "SML_comment"; diff -r c85e018be3a3 -r e670969f34df src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Dec 08 22:42:12 2014 +0100 @@ -241,6 +241,7 @@ val ML_NUMERAL = "ML_numeral" val ML_CHAR = "ML_char" val ML_STRING = "ML_string" + val ML_CARTOUCHE = "ML_cartouche" val ML_COMMENT = "ML_comment" val SML_STRING = "SML_string" val SML_COMMENT = "SML_comment" diff -r c85e018be3a3 -r e670969f34df src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Dec 08 16:04:50 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Mon Dec 08 22:42:12 2014 +0100 @@ -106,6 +106,7 @@ ML_Lex.Kind.CHAR -> LITERAL2, ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, + ML_Lex.Kind.CARTOUCHE -> COMMENT4, ML_Lex.Kind.COMMENT -> COMMENT1, ML_Lex.Kind.ANTIQ -> NULL, ML_Lex.Kind.ANTIQ_START -> LITERAL4, @@ -727,6 +728,7 @@ Markup.ML_NUMERAL -> inner_numeral_color, Markup.ML_CHAR -> inner_quoted_color, Markup.ML_STRING -> inner_quoted_color, + Markup.ML_CARTOUCHE -> inner_cartouche_color, Markup.ML_COMMENT -> inner_comment_color, Markup.SML_STRING -> inner_quoted_color, Markup.SML_COMMENT -> inner_comment_color)