src/Pure/Isar/proof_context.ML
changeset 42204 b3277168c1e7
parent 42173 5d33c12ccf22
child 42223 098c86e53153
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -65,7 +65,9 @@
     1.4    val allow_dummies: Proof.context -> Proof.context
     1.5    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     1.6    val check_tfree: Proof.context -> string * sort -> string * sort
     1.7 -  val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
     1.8 +  val type_context: Proof.context -> Syntax.type_context
     1.9 +  val term_context: Proof.context -> Syntax.term_context
    1.10 +  val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
    1.11    val standard_infer_types: Proof.context -> term list -> term list
    1.12    val read_term_pattern: Proof.context -> string -> term
    1.13    val read_term_schematic: Proof.context -> string -> term
    1.14 @@ -665,12 +667,18 @@
    1.15  
    1.16  in
    1.17  
    1.18 +fun type_context ctxt : Syntax.type_context =
    1.19 + {get_class = read_class ctxt,
    1.20 +  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
    1.21 +  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
    1.22 +  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
    1.23 +
    1.24  fun term_context ctxt : Syntax.term_context =
    1.25   {get_sort = get_sort ctxt,
    1.26    get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
    1.27      handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
    1.28    get_free = intern_skolem ctxt (Variable.def_type ctxt false),
    1.29 -  markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
    1.30 +  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
    1.31    markup_free = fn x =>
    1.32      [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    1.33      (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
    1.34 @@ -748,14 +756,16 @@
    1.35  fun parse_sort ctxt text =
    1.36    let
    1.37      val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    1.38 -    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
    1.39 +    val S =
    1.40 +      Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
    1.41        handle ERROR msg => parse_failed ctxt pos msg "sort";
    1.42    in Type.minimize_sort (tsig_of ctxt) S end;
    1.43  
    1.44  fun parse_typ ctxt text =
    1.45    let
    1.46      val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    1.47 -    val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
    1.48 +    val T =
    1.49 +      Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
    1.50        handle ERROR msg => parse_failed ctxt pos msg "type";
    1.51    in T end;
    1.52  
    1.53 @@ -777,8 +787,9 @@
    1.54      fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
    1.55        handle ERROR msg => SOME msg;
    1.56      val t =
    1.57 -      Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
    1.58 -        handle ERROR msg => parse_failed ctxt pos msg kind;
    1.59 +      Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
    1.60 +        root (syms, pos)
    1.61 +      handle ERROR msg => parse_failed ctxt pos msg kind;
    1.62    in t end;
    1.63  
    1.64  
    1.65 @@ -1079,13 +1090,6 @@
    1.66  
    1.67  (* authentic syntax *)
    1.68  
    1.69 -val _ = Context.>>
    1.70 -  (Context.map_theory
    1.71 -    (Sign.add_advanced_trfuns
    1.72 -      (Syntax.type_ast_trs
    1.73 -        {read_class = read_class,
    1.74 -          read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
    1.75 -
    1.76  local
    1.77  
    1.78  fun const_ast_tr intern ctxt [Syntax.Variable c] =