# HG changeset patch # User wenzelm # Date 1408118554 -7200 # Node ID fff8d328da5665d0bc199c28bf6134282b83f12b # Parent 52c68f8126a8124f0f2032f862eff1633bd26006 more informative Token.Name with history of morphisms; tuned signature; diff -r 52c68f8126a8 -r fff8d328da56 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Aug 14 19:55:00 2014 +0200 +++ b/src/Pure/Isar/args.ML Fri Aug 15 18:02:34 2014 +0200 @@ -43,12 +43,11 @@ val symbol: string parser val liberal_name: string parser val var: indexname parser - val internal_text: string parser + val internal_name: (string * morphism) parser val internal_typ: typ parser val internal_term: term parser val internal_fact: thm list parser val internal_attribute: (morphism -> attribute) parser - val named_text: (string -> string) -> string parser val named_typ: (string -> typ) -> typ parser val named_term: (string -> term) -> term parser val named_fact: (string -> string option * thm list) -> thm list parser @@ -97,17 +96,7 @@ (case output_info of NONE => Pretty.str name | SOME (_, markup) => Pretty.mark_str (markup, name)); - val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; - fun prt_arg arg = - (case Token.get_value arg of - SOME (Token.Literal markup) => - let val x = Token.content_of arg - in Pretty.mark_str (Token.keyword_markup markup x, x) end - | SOME (Token.Text s) => Pretty.str (quote s) - | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T - | SOME (Token.Term t) => Syntax.pretty_term ctxt t - | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) - | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg)); + val prt_arg = Token.pretty_value ctxt; in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end; @@ -127,12 +116,7 @@ fun map_args f (Src {name, args, output_info}) = Src {name = name, args = map f args, output_info = output_info}; -fun transform_values phi = map_args (Token.map_value - (fn Token.Typ T => Token.Typ (Morphism.typ phi T) - | Token.Term t => Token.Term (Morphism.term phi t) - | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths) - | Token.Attribute att => Token.Attribute (Morphism.transform phi att) - | tok => tok)); +val transform_values = map_args o Token.transform_value; val init_assignable = map_args Token.init_assignable; val closure = map_args Token.closure; @@ -209,13 +193,12 @@ fun evaluate mk eval arg = let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end; -val internal_text = value (fn Token.Text s => s); +val internal_name = value (fn Token.Name a => a); val internal_typ = value (fn Token.Typ T => T); val internal_term = value (fn Token.Term t => t); val internal_fact = value (fn Token.Fact (_, ths) => ths); val internal_attribute = value (fn Token.Attribute att => att); -fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of); fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of); fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of); @@ -267,7 +250,7 @@ fun attribs check = let fun intern tok = check (Token.content_of tok, Token.pos_of tok); - val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern; + val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern; val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src; in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end; diff -r 52c68f8126a8 -r fff8d328da56 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Aug 14 19:55:00 2014 +0200 +++ b/src/Pure/Isar/token.ML Fri Aug 15 18:02:34 2014 +0200 @@ -12,9 +12,14 @@ Error of string | Sync | EOF type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} datatype value = - Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | + Literal of bool * Markup.T | + Name of string * morphism | + Typ of typ | + Term of term | Fact of string option * thm list | - Attribute of morphism -> attribute | Files of file Exn.result list + Attribute of morphism -> attribute | + Files of file Exn.result list + val name0: string -> value type T val str_of_kind: kind -> string val pos_of: T -> Position.T @@ -49,17 +54,19 @@ val markup: T -> Markup.T val unparse: T -> string val print: T -> string + val pretty_value: Proof.context -> T -> Pretty.T val text_of: T -> string * string val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_value: T -> value option val map_value: (value -> value) -> T -> T val reports_of_value: T -> Position.report list - val mk_text: string -> T + val mk_name: string -> T val mk_typ: typ -> T val mk_term: term -> T val mk_fact: string option * thm list -> T val mk_attribute: (morphism -> attribute) -> T + val transform_value: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> unit val closure: T -> T @@ -89,13 +96,15 @@ datatype value = Literal of bool * Markup.T | - Text of string | + Name of string * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Files of file Exn.result list; +fun name0 a = Name (a, Morphism.identity); + datatype slot = Slot | Value of value option | @@ -341,17 +350,46 @@ | _ => []); +(* pretty value *) + +fun pretty_value ctxt tok = + (case get_value tok of + SOME (Literal markup) => + let val x = content_of tok + in Pretty.mark_str (keyword_markup markup x, x) end + | SOME (Name (a, _)) => Pretty.str (quote a) + | SOME (Typ T) => Syntax.pretty_typ ctxt T + | SOME (Term t) => Syntax.pretty_term ctxt t + | SOME (Fact (_, ths)) => + Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths)) + | _ => Pretty.mark_str (markup tok, unparse tok)); + + (* make values *) fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v)); -val mk_text = mk_value "" o Text; +val mk_name = mk_value "" o name0; val mk_typ = mk_value "" o Typ; val mk_term = mk_value "" o Term; val mk_fact = mk_value "" o Fact; val mk_attribute = mk_value "" o Attribute; +(* transform value *) + +fun transform_value phi = + map_value (fn v => + (case v of + Literal _ => v + | Name (a, psi) => Name (a, psi $> phi) + | Typ T => Typ (Morphism.typ phi T) + | Term t => Term (Morphism.term phi t) + | Fact (a, ths) => Fact (a, Morphism.fact phi ths) + | Attribute att => Attribute (Morphism.transform phi att) + | Files _ => v)); + + (* static binding *) (*1st stage: initialize assignable slots*)