ContextPosition.report;
authorwenzelm
Mon Sep 29 14:41:25 2008 +0200 (2008-09-29 ago)
changeset 28407f9db1da584ac
parent 28406 daeb21fec18f
child 28408 e26aac53723d
ContextPosition.report;
parse_token/report_token: explicit context;
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_context.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax.ML
     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
     2.1 --- a/src/Pure/ML/ml_context.ML	Mon Sep 29 14:41:24 2008 +0200
     2.2 +++ b/src/Pure/ML/ml_context.ML	Mon Sep 29 14:41:25 2008 +0200
     2.3 @@ -173,7 +173,7 @@
     2.4    let val ((name, _), pos) = Args.dest_src src in
     2.5      (case Symtab.lookup (! global_parsers) name of
     2.6        NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
     2.7 -    | SOME scan => (Position.report (Markup.ML_antiq name) pos;
     2.8 +    | SOME scan => (ContextPosition.report ctxt (Markup.ML_antiq name) pos;
     2.9          Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
    2.10    end;
    2.11  
     3.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Sep 29 14:41:24 2008 +0200
     3.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 29 14:41:25 2008 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4    val tvarT: typ
     3.5    val terminals: string list
     3.6    val is_terminal: string -> bool
     3.7 -  val report_token: token -> unit
     3.8 +  val report_token: Proof.context -> token -> unit
     3.9    val matching_tokens: token * token -> bool
    3.10    val valued_token: token -> bool
    3.11    val predef_term: string -> token option
    3.12 @@ -162,8 +162,8 @@
    3.13    | Comment     => Markup.inner_comment
    3.14    | EOF         => Markup.none;
    3.15  
    3.16 -fun report_token (Token (kind, _, (pos, _))) =
    3.17 -  Position.report (token_kind_markup kind) pos;
    3.18 +fun report_token ctxt (Token (kind, _, (pos, _))) =
    3.19 +  ContextPosition.report ctxt (token_kind_markup kind) pos;
    3.20  
    3.21  
    3.22  (* matching_tokens *)
     4.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:24 2008 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:25 2008 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4      (string * string) trrule list -> syntax -> syntax
     4.5    val update_trrules_i: ast trrule list -> syntax -> syntax
     4.6    val remove_trrules_i: ast trrule list -> syntax -> syntax
     4.7 -  val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
     4.8 +  val parse_token: Proof.context -> Markup.T -> string -> SymbolPos.T list * Position.T
     4.9    val parse_sort: Proof.context -> string -> sort
    4.10    val parse_typ: Proof.context -> string -> typ
    4.11    val parse_term: Proof.context -> string -> term
    4.12 @@ -482,7 +482,7 @@
    4.13    let
    4.14      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    4.15      val toks = Lexicon.tokenize lexicon xids syms;
    4.16 -    val _ = List.app Lexicon.report_token toks;
    4.17 +    val _ = List.app (Lexicon.report_token ctxt) toks;
    4.18  
    4.19      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    4.20      val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
    4.21 @@ -695,10 +695,10 @@
    4.22  
    4.23  (* (un)parsing *)
    4.24  
    4.25 -fun parse_token markup str =
    4.26 +fun parse_token ctxt markup str =
    4.27    let
    4.28      val (syms, pos) = read_token str;
    4.29 -    val _ = Position.report markup pos;
    4.30 +    val _ = ContextPosition.report ctxt markup pos;
    4.31    in (syms, pos) end;
    4.32  
    4.33  local