1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 06 14:44:40 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 06 15:10:39 2011 +0200
     1.3 @@ -64,14 +64,11 @@
     1.4    val read_const_proper: Proof.context -> bool -> string -> term
     1.5    val read_const: Proof.context -> bool -> typ -> string -> term
     1.6    val allow_dummies: Proof.context -> Proof.context
     1.7 +  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
     1.8    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     1.9    val check_tfree: Proof.context -> string * sort -> string * sort
    1.10 -  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
    1.11 -  type type_context
    1.12 -  val type_context: Proof.context -> type_context
    1.13 -  type term_context
    1.14 -  val term_context: Proof.context -> term_context
    1.15    val standard_infer_types: Proof.context -> term list -> term list
    1.16 +  val intern_skolem: Proof.context -> string -> string option
    1.17    val read_term_pattern: Proof.context -> string -> term
    1.18    val read_term_schematic: Proof.context -> string -> term
    1.19    val read_term_abbrev: Proof.context -> string -> term
    1.20 @@ -266,7 +263,6 @@
    1.21  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.22  
    1.23  val consts_of = #1 o #consts o rep_context;
    1.24 -val const_space = Consts.space_of o consts_of;
    1.25  val the_const_constraint = Consts.the_constraint o consts_of;
    1.26  
    1.27  val facts_of = #facts o rep_context;
    1.28 @@ -526,6 +522,22 @@
    1.29  end;
    1.30  
    1.31  
    1.32 +(* skolem variables *)
    1.33 +
    1.34 +fun intern_skolem ctxt x =
    1.35 +  let
    1.36 +    val _ = no_skolem false x;
    1.37 +    val sko = lookup_skolem ctxt x;
    1.38 +    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.39 +    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    1.40 +  in
    1.41 +    if Variable.is_const ctxt x then NONE
    1.42 +    else if is_some sko then sko
    1.43 +    else if not is_const orelse is_declared then SOME x
    1.44 +    else NONE
    1.45 +  end;
    1.46 +
    1.47 +
    1.48  (* read_term *)
    1.49  
    1.50  fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
    1.51 @@ -618,9 +630,7 @@
    1.52  end;
    1.53  
    1.54  
    1.55 -(* decoding raw terms (syntax trees) *)
    1.56 -
    1.57 -(* types *)
    1.58 +(* sort constraints *)
    1.59  
    1.60  fun get_sort ctxt raw_text =
    1.61    let
    1.62 @@ -653,54 +663,6 @@
    1.63  fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
    1.64  fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
    1.65  
    1.66 -local
    1.67 -
    1.68 -fun intern_skolem ctxt def_type x =
    1.69 -  let
    1.70 -    val _ = no_skolem false x;
    1.71 -    val sko = lookup_skolem ctxt x;
    1.72 -    val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.73 -    val is_declared = is_some (def_type (x, ~1));
    1.74 -  in
    1.75 -    if Variable.is_const ctxt x then NONE
    1.76 -    else if is_some sko then sko
    1.77 -    else if not is_const orelse is_declared then SOME x
    1.78 -    else NONE
    1.79 -  end;
    1.80 -
    1.81 -in
    1.82 -
    1.83 -type type_context =
    1.84 - {get_class: string -> string,
    1.85 -  get_type: string -> string,
    1.86 -  markup_class: string -> Markup.T list,
    1.87 -  markup_type: string -> Markup.T list};
    1.88 -
    1.89 -fun type_context ctxt : type_context =
    1.90 - {get_class = read_class ctxt,
    1.91 -  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
    1.92 -  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
    1.93 -  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
    1.94 -
    1.95 -type term_context =
    1.96 - {get_const: string -> bool * string,
    1.97 -  get_free: string -> string option,
    1.98 -  markup_const: string -> Markup.T list,
    1.99 -  markup_free: string -> Markup.T list,
   1.100 -  markup_var: indexname -> Markup.T list};
   1.101 -
   1.102 -fun term_context ctxt : term_context =
   1.103 - {get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
   1.104 -    handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   1.105 -  get_free = intern_skolem ctxt (Variable.def_type ctxt false),
   1.106 -  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
   1.107 -  markup_free = fn x =>
   1.108 -    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
   1.109 -    (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
   1.110 -  markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
   1.111 -
   1.112 -end;
   1.113 -
   1.114  
   1.115  (* certify terms *)
   1.116  

     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 14:44:40 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:10:39 2011 +0200
     2.3 @@ -93,7 +93,12 @@
     2.4  
     2.5  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
     2.6    let
     2.7 -    val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt;
     2.8 +    val tsig = ProofContext.tsig_of ctxt;
     2.9 +
    2.10 +    val get_class = ProofContext.read_class ctxt;
    2.11 +    val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
    2.12 +    fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c];
    2.13 +    fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c];
    2.14  
    2.15      val reports = Unsynchronized.ref ([]: Position.reports);
    2.16      fun report pos = Position.reports reports [pos];
    2.17 @@ -146,14 +151,23 @@
    2.18  
    2.19  (* decode_term -- transform parse tree into raw term *)
    2.20  
    2.21 -fun markup_bound def id =
    2.22 -  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
    2.23 -
    2.24  fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
    2.25    | decode_term ctxt (reports0, Exn.Result tm) =
    2.26        let
    2.27 -        val {get_const, get_free, markup_const, markup_free, markup_var} =
    2.28 -          ProofContext.term_context ctxt;
    2.29 +        val consts = ProofContext.consts_of ctxt;
    2.30 +        fun get_const a =
    2.31 +          ((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
    2.32 +            handle ERROR _ => (false, Consts.intern consts a));
    2.33 +        val get_free = ProofContext.intern_skolem ctxt;
    2.34 +        fun markup_const c = [Name_Space.markup_entry (Consts.space_of consts) c];
    2.35 +        fun markup_free x =
    2.36 +          [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    2.37 +          (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
    2.38 +           else [Markup.hilite]);
    2.39 +        fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
    2.40 +        fun markup_bound def id =
    2.41 +          [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
    2.42 +
    2.43          val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
    2.44  
    2.45          val reports = Unsynchronized.ref reports0;