src/Pure/Isar/proof_context.ML
changeset 28411 93ec7fa3b3a0
parent 28407 f9db1da584ac
child 28417 74e580c6f2b5
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:26:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 29 21:26:36 2008 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4      (case Variable.lookup_const ctxt c of
     1.5        SOME d => Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => error msg)
     1.6      | NONE => Consts.read_const (consts_of ctxt) c)
     1.7 -  in ContextPosition.report ctxt (Markup.const d) pos; t end;
     1.8 +  in Position.report (Markup.const d) pos; t end;
     1.9  
    1.10  in
    1.11  
    1.12 @@ -453,12 +453,12 @@
    1.13      val (c, pos) = token_content str;
    1.14    in
    1.15      if Syntax.is_tid c then
    1.16 -     (ContextPosition.report ctxt Markup.tfree pos;
    1.17 +     (Position.report Markup.tfree pos;
    1.18        TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
    1.19      else
    1.20        let
    1.21          val d = Sign.intern_type thy c;
    1.22 -        val _ = ContextPosition.report ctxt (Markup.tycon d) pos;
    1.23 +        val _ = Position.report (Markup.tycon d) pos;
    1.24        in Type (d, replicate (Sign.arity_number thy d) dummyT) end
    1.25    end;
    1.26  
    1.27 @@ -468,7 +468,7 @@
    1.28    let val (c, pos) = token_content str in
    1.29      (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    1.30        (SOME x, false) =>
    1.31 -        (ContextPosition.report ctxt (Markup.name x
    1.32 +        (Position.report (Markup.name x
    1.33              (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
    1.34            Free (x, infer_type ctxt x))
    1.35      | _ => prep_const_proper ctxt (c, pos))
    1.36 @@ -687,7 +687,7 @@
    1.37  
    1.38  fun parse_sort ctxt text =
    1.39    let
    1.40 -    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    1.41 +    val (syms, pos) = Syntax.parse_token Markup.sort text;
    1.42      val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
    1.43          (Sign.intern_sort (theory_of ctxt)) (syms, pos)
    1.44        handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    1.45 @@ -698,7 +698,7 @@
    1.46      val thy = ProofContext.theory_of ctxt;
    1.47      val get_sort = get_sort thy (Variable.def_sort ctxt);
    1.48  
    1.49 -    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    1.50 +    val (syms, pos) = Syntax.parse_token Markup.typ text;
    1.51      val T = Sign.intern_tycons thy
    1.52          (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
    1.53        handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
    1.54 @@ -711,7 +711,7 @@
    1.55  
    1.56      val (T', _) = TypeInfer.paramify_dummies T 0;
    1.57      val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    1.58 -    val (syms, pos) = Syntax.parse_token ctxt markup text;
    1.59 +    val (syms, pos) = Syntax.parse_token markup text;
    1.60  
    1.61      fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
    1.62        handle ERROR msg => SOME msg;
    1.63 @@ -932,7 +932,7 @@
    1.64            if name = "" then [Thm.transfer thy Drule.dummy_thm]
    1.65            else
    1.66              (case Facts.lookup (Context.Proof ctxt) local_facts name of
    1.67 -              SOME (_, ths) => (ContextPosition.report ctxt (Markup.local_fact name) pos;
    1.68 +              SOME (_, ths) => (Position.report (Markup.local_fact name) pos;
    1.69                  map (Thm.transfer thy) (Facts.select thmref ths))
    1.70              | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    1.71        in pick name thms end;
    1.72 @@ -971,7 +971,7 @@
    1.73      val bname = Name.name_of binding;
    1.74      val pos = Name.pos_of binding;
    1.75      val name = full_name ctxt bname;
    1.76 -    val _ = ContextPosition.report ctxt (Markup.local_fact_decl name) pos;
    1.77 +    val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
    1.78  
    1.79      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    1.80      fun app (th, attrs) x =
    1.81 @@ -1118,7 +1118,7 @@
    1.82        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    1.83        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    1.84      val _ = (vars ~~ xs') |> List.app (fn ((binding, _, _), x') =>
    1.85 -      ContextPosition.report ctxt (Markup.fixed_decl x') (Name.pos_of binding));
    1.86 +      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Name.pos_of binding));
    1.87    in (xs', ctxt'') end;
    1.88  
    1.89  in