src/Pure/Isar/proof_context.ML
changeset 27821 0ead8c2428f9
parent 27785 3bf65bfda540
child 27828 edafacb690a3
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Aug 10 12:38:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Aug 10 12:38:25 2008 +0200
     1.3 @@ -411,24 +411,47 @@
     1.4  
     1.5  (* type and constant names *)
     1.6  
     1.7 -fun read_tyname ctxt c =
     1.8 -  if Syntax.is_tid c then
     1.9 -    TFree (c, the_default (Sign.defaultS (theory_of ctxt)) (Variable.def_sort ctxt (c, ~1)))
    1.10 -  else
    1.11 -    let
    1.12 -      val thy = theory_of ctxt;
    1.13 -      val d = Sign.intern_type thy c;
    1.14 -    in Type (d, replicate (Sign.arity_number thy d) dummyT) end;
    1.15 +local
    1.16 +
    1.17 +val token_content = Syntax.read_token #>> SymbolPos.content;
    1.18 +
    1.19 +fun prep_const_proper ctxt (c, pos) =
    1.20 +  let val t as (Const (d, _)) =
    1.21 +    (case Variable.lookup_const ctxt c of
    1.22 +      SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
    1.23 +    | NONE => Consts.read_const (consts_of ctxt) c)
    1.24 +  in Position.report (Markup.const d) pos; t end;
    1.25 +
    1.26 +in
    1.27  
    1.28 -fun read_const_proper ctxt c =
    1.29 -  (case Variable.lookup_const ctxt c of
    1.30 -    SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
    1.31 -  | NONE => Consts.read_const (consts_of ctxt) c);
    1.32 +fun read_tyname ctxt str =
    1.33 +  let
    1.34 +    val thy = theory_of ctxt;
    1.35 +    val (c, pos) = token_content str;
    1.36 +  in
    1.37 +    if Syntax.is_tid c then
    1.38 +     (Position.report Markup.tfree pos;
    1.39 +      TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
    1.40 +    else
    1.41 +      let
    1.42 +        val d = Sign.intern_type thy c;
    1.43 +        val _ = Position.report (Markup.tycon d) pos;
    1.44 +      in Type (d, replicate (Sign.arity_number thy d) dummyT) end
    1.45 +  end;
    1.46  
    1.47 -fun read_const ctxt c =
    1.48 -  (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    1.49 -    (SOME x, false) => Free (x, infer_type ctxt x)
    1.50 -  | _ => read_const_proper ctxt c);
    1.51 +fun read_const_proper ctxt = prep_const_proper ctxt o token_content;
    1.52 +
    1.53 +fun read_const ctxt str =
    1.54 +  let val (c, pos) = token_content str in
    1.55 +    (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    1.56 +      (SOME x, false) =>
    1.57 +        (Position.report (Markup.name x
    1.58 +            (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
    1.59 +          Free (x, infer_type ctxt x))
    1.60 +    | _ => prep_const_proper ctxt (c, pos))
    1.61 +  end;
    1.62 +
    1.63 +end;
    1.64  
    1.65  
    1.66  (* read_term *)
    1.67 @@ -639,15 +662,9 @@
    1.68  
    1.69  local
    1.70  
    1.71 -fun parse_token markup str =
    1.72 -  let
    1.73 -    val (syms, pos) = Syntax.read_token str;
    1.74 -    val _ = Position.report markup pos;
    1.75 -  in (syms, pos) end;
    1.76 -
    1.77  fun parse_sort ctxt text =
    1.78    let
    1.79 -    val (syms, pos) = parse_token Markup.sort text;
    1.80 +    val (syms, pos) = Syntax.parse_token Markup.sort text;
    1.81      val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
    1.82          (Sign.intern_sort (theory_of ctxt)) (syms, pos)
    1.83        handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    1.84 @@ -658,7 +675,7 @@
    1.85      val thy = ProofContext.theory_of ctxt;
    1.86      val get_sort = get_sort thy (Variable.def_sort ctxt);
    1.87  
    1.88 -    val (syms, pos) = parse_token Markup.typ text;
    1.89 +    val (syms, pos) = Syntax.parse_token Markup.typ text;
    1.90      val T = Sign.intern_tycons thy
    1.91          (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
    1.92        handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
    1.93 @@ -670,8 +687,8 @@
    1.94      val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
    1.95  
    1.96      val (T', _) = TypeInfer.paramify_dummies T 0;
    1.97 -    val markup as (kind, _) = if T' = propT then Markup.proposition else Markup.term;
    1.98 -    val (syms, pos) = parse_token markup text;
    1.99 +    val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
   1.100 +    val (syms, pos) = Syntax.parse_token markup text;
   1.101  
   1.102      fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
   1.103        handle ERROR msg => SOME msg;
   1.104 @@ -873,11 +890,13 @@
   1.105          val local_facts = facts_of ctxt;
   1.106          val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
   1.107          val name = Facts.name_of_ref thmref;
   1.108 +        val pos = Facts.pos_of_ref xthmref;
   1.109          val thms =
   1.110            if name = "" then [Thm.transfer thy Drule.dummy_thm]
   1.111            else
   1.112              (case Facts.lookup (Context.Proof ctxt) local_facts name of
   1.113 -              SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths)
   1.114 +              SOME (_, ths) => (Position.report (Markup.local_fact name) pos;
   1.115 +                map (Thm.transfer thy) (Facts.select thmref ths))
   1.116              | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
   1.117        in pick name thms end;
   1.118