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