more informative Token.Name with history of morphisms;
authorwenzelm
Fri Aug 15 18:02:34 2014 +0200 (2014-08-15)
changeset 57944fff8d328da56
parent 57943 52c68f8126a8
child 57945 cacb00a569e0
more informative Token.Name with history of morphisms;
tuned signature;
src/Pure/Isar/args.ML
src/Pure/Isar/token.ML
     1.1 --- a/src/Pure/Isar/args.ML	Thu Aug 14 19:55:00 2014 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 15 18:02:34 2014 +0200
     1.3 @@ -43,12 +43,11 @@
     1.4    val symbol: string parser
     1.5    val liberal_name: string parser
     1.6    val var: indexname parser
     1.7 -  val internal_text: string parser
     1.8 +  val internal_name: (string * morphism) parser
     1.9    val internal_typ: typ parser
    1.10    val internal_term: term parser
    1.11    val internal_fact: thm list parser
    1.12    val internal_attribute: (morphism -> attribute) parser
    1.13 -  val named_text: (string -> string) -> string parser
    1.14    val named_typ: (string -> typ) -> typ parser
    1.15    val named_term: (string -> term) -> term parser
    1.16    val named_fact: (string -> string option * thm list) -> thm list parser
    1.17 @@ -97,17 +96,7 @@
    1.18        (case output_info of
    1.19          NONE => Pretty.str name
    1.20        | SOME (_, markup) => Pretty.mark_str (markup, name));
    1.21 -    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    1.22 -    fun prt_arg arg =
    1.23 -      (case Token.get_value arg of
    1.24 -        SOME (Token.Literal markup) =>
    1.25 -          let val x = Token.content_of arg
    1.26 -          in Pretty.mark_str (Token.keyword_markup markup x, x) end
    1.27 -      | SOME (Token.Text s) => Pretty.str (quote s)
    1.28 -      | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
    1.29 -      | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    1.30 -      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    1.31 -      | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    1.32 +    val prt_arg = Token.pretty_value ctxt;
    1.33    in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
    1.34  
    1.35  
    1.36 @@ -127,12 +116,7 @@
    1.37  fun map_args f (Src {name, args, output_info}) =
    1.38    Src {name = name, args = map f args, output_info = output_info};
    1.39  
    1.40 -fun transform_values phi = map_args (Token.map_value
    1.41 -  (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
    1.42 -    | Token.Term t => Token.Term (Morphism.term phi t)
    1.43 -    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
    1.44 -    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
    1.45 -    | tok => tok));
    1.46 +val transform_values = map_args o Token.transform_value;
    1.47  
    1.48  val init_assignable = map_args Token.init_assignable;
    1.49  val closure = map_args Token.closure;
    1.50 @@ -209,13 +193,12 @@
    1.51  fun evaluate mk eval arg =
    1.52    let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
    1.53  
    1.54 -val internal_text = value (fn Token.Text s => s);
    1.55 +val internal_name = value (fn Token.Name a => a);
    1.56  val internal_typ = value (fn Token.Typ T => T);
    1.57  val internal_term = value (fn Token.Term t => t);
    1.58  val internal_fact = value (fn Token.Fact (_, ths) => ths);
    1.59  val internal_attribute = value (fn Token.Attribute att => att);
    1.60  
    1.61 -fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    1.62  fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
    1.63  fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
    1.64  
    1.65 @@ -267,7 +250,7 @@
    1.66  fun attribs check =
    1.67    let
    1.68      fun intern tok = check (Token.content_of tok, Token.pos_of tok);
    1.69 -    val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
    1.70 +    val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
    1.71      val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
    1.72    in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
    1.73  
     2.1 --- a/src/Pure/Isar/token.ML	Thu Aug 14 19:55:00 2014 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Fri Aug 15 18:02:34 2014 +0200
     2.3 @@ -12,9 +12,14 @@
     2.4      Error of string | Sync | EOF
     2.5    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
     2.6    datatype value =
     2.7 -    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
     2.8 +    Literal of bool * Markup.T |
     2.9 +    Name of string * morphism |
    2.10 +    Typ of typ |
    2.11 +    Term of term |
    2.12      Fact of string option * thm list |
    2.13 -    Attribute of morphism -> attribute | Files of file Exn.result list
    2.14 +    Attribute of morphism -> attribute |
    2.15 +    Files of file Exn.result list
    2.16 +  val name0: string -> value
    2.17    type T
    2.18    val str_of_kind: kind -> string
    2.19    val pos_of: T -> Position.T
    2.20 @@ -49,17 +54,19 @@
    2.21    val markup: T -> Markup.T
    2.22    val unparse: T -> string
    2.23    val print: T -> string
    2.24 +  val pretty_value: Proof.context -> T -> Pretty.T
    2.25    val text_of: T -> string * string
    2.26    val get_files: T -> file Exn.result list
    2.27    val put_files: file Exn.result list -> T -> T
    2.28    val get_value: T -> value option
    2.29    val map_value: (value -> value) -> T -> T
    2.30    val reports_of_value: T -> Position.report list
    2.31 -  val mk_text: string -> T
    2.32 +  val mk_name: string -> T
    2.33    val mk_typ: typ -> T
    2.34    val mk_term: term -> T
    2.35    val mk_fact: string option * thm list -> T
    2.36    val mk_attribute: (morphism -> attribute) -> T
    2.37 +  val transform_value: morphism -> T -> T
    2.38    val init_assignable: T -> T
    2.39    val assign: value option -> T -> unit
    2.40    val closure: T -> T
    2.41 @@ -89,13 +96,15 @@
    2.42  
    2.43  datatype value =
    2.44    Literal of bool * Markup.T |
    2.45 -  Text of string |
    2.46 +  Name of string * morphism |
    2.47    Typ of typ |
    2.48    Term of term |
    2.49    Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
    2.50    Attribute of morphism -> attribute |
    2.51    Files of file Exn.result list;
    2.52  
    2.53 +fun name0 a = Name (a, Morphism.identity);
    2.54 +
    2.55  datatype slot =
    2.56    Slot |
    2.57    Value of value option |
    2.58 @@ -341,17 +350,46 @@
    2.59    | _ => []);
    2.60  
    2.61  
    2.62 +(* pretty value *)
    2.63 +
    2.64 +fun pretty_value ctxt tok =
    2.65 +  (case get_value tok of
    2.66 +    SOME (Literal markup) =>
    2.67 +      let val x = content_of tok
    2.68 +      in Pretty.mark_str (keyword_markup markup x, x) end
    2.69 +  | SOME (Name (a, _)) => Pretty.str (quote a)
    2.70 +  | SOME (Typ T) => Syntax.pretty_typ ctxt T
    2.71 +  | SOME (Term t) => Syntax.pretty_term ctxt t
    2.72 +  | SOME (Fact (_, ths)) =>
    2.73 +      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
    2.74 +  | _ => Pretty.mark_str (markup tok, unparse tok));
    2.75 +
    2.76 +
    2.77  (* make values *)
    2.78  
    2.79  fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
    2.80  
    2.81 -val mk_text = mk_value "<text>" o Text;
    2.82 +val mk_name = mk_value "<name>" o name0;
    2.83  val mk_typ = mk_value "<typ>" o Typ;
    2.84  val mk_term = mk_value "<term>" o Term;
    2.85  val mk_fact = mk_value "<fact>" o Fact;
    2.86  val mk_attribute = mk_value "<attribute>" o Attribute;
    2.87  
    2.88  
    2.89 +(* transform value *)
    2.90 +
    2.91 +fun transform_value phi =
    2.92 +  map_value (fn v =>
    2.93 +    (case v of
    2.94 +      Literal _ => v
    2.95 +    | Name (a, psi) => Name (a, psi $> phi)
    2.96 +    | Typ T => Typ (Morphism.typ phi T)
    2.97 +    | Term t => Term (Morphism.term phi t)
    2.98 +    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
    2.99 +    | Attribute att => Attribute (Morphism.transform phi att)
   2.100 +    | Files _ => v));
   2.101 +
   2.102 +
   2.103  (* static binding *)
   2.104  
   2.105  (*1st stage: initialize assignable slots*)