# HG changeset patch # User wenzelm # Date 1281290094 -7200 # Node ID 8b0383334031a0ff2b8666462ccf7a5b3d0c795a # Parent d8c7be27e01d542a91eff067b61e63553ae3219a prefer Context_Position.report where a proper context is available -- notably for "inner" entities; diff -r d8c7be27e01d -r 8b0383334031 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Aug 08 19:36:31 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Aug 08 19:54:54 2010 +0200 @@ -334,7 +334,7 @@ val (syms, pos) = Syntax.read_token text; val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms)) handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); - val _ = Position.report (Markup.tclass c) pos; + val _ = Context_Position.report ctxt (Markup.tclass c) pos; in c end; @@ -469,7 +469,7 @@ val _ = if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg else (); - val _ = Position.report (Markup.const d) pos; + val _ = Context_Position.report ctxt (Markup.const d) pos; in t end; in @@ -480,13 +480,13 @@ val (c, pos) = token_content text; in if Syntax.is_tid c then - (Position.report Markup.tfree pos; + (Context_Position.report ctxt Markup.tfree pos; TFree (c, default_sort ctxt (c, ~1))) else let val d = Type.intern_type tsig c; val decl = Type.the_decl tsig d; - val _ = Position.report (Markup.tycon d) pos; + val _ = Context_Position.report ctxt (Markup.tycon d) pos; fun err () = error ("Bad type name: " ^ quote d); val args = (case decl of @@ -511,7 +511,7 @@ in (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of (SOME x, false) => - (Position.report (Markup.name x + (Context_Position.report ctxt (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos; Free (x, infer_type ctxt (x, ty))) | _ => prep_const_proper ctxt strict (c, pos)) @@ -977,7 +977,7 @@ if name = "" then [Thm.transfer thy Drule.dummy_thm] else (case Facts.lookup (Context.Proof ctxt) local_facts name of - SOME (_, ths) => (Position.report (Markup.local_fact name) pos; + SOME (_, ths) => (Context_Position.report ctxt (Markup.local_fact name) pos; map (Thm.transfer thy) (Facts.select thmref ths)) | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref); in pick name thms end; @@ -1007,7 +1007,7 @@ let val pos = Binding.pos_of b; val name = full_name ctxt b; - val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos; + val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos; val facts = PureThy.name_thmss false name raw_facts; fun app (th, attrs) x = @@ -1186,7 +1186,7 @@ |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed)); val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') => - Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b)); + Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b)); in (xs', ctxt'') end; diff -r d8c7be27e01d -r 8b0383334031 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sun Aug 08 19:36:31 2010 +0200 +++ b/src/Pure/ML/ml_context.ML Sun Aug 08 19:54:54 2010 +0200 @@ -105,7 +105,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_parsers) name of NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME scan => (Position.report (Markup.ML_antiq name) pos; + | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos; Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) end; diff -r d8c7be27e01d -r 8b0383334031 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Sun Aug 08 19:36:31 2010 +0200 +++ b/src/Pure/Syntax/lexicon.ML Sun Aug 08 19:54:54 2010 +0200 @@ -65,7 +65,7 @@ val tvarT: typ val terminals: string list val is_terminal: string -> bool - val report_token: token -> unit + val report_token: Proof.context -> token -> unit val matching_tokens: token * token -> bool val valued_token: token -> bool val predef_term: string -> token option @@ -185,8 +185,8 @@ | Comment => Markup.inner_comment | EOF => Markup.none; -fun report_token (Token (kind, _, (pos, _))) = - Position.report (token_kind_markup kind) pos; +fun report_token ctxt (Token (kind, _, (pos, _))) = + Context_Position.report ctxt (token_kind_markup kind) pos; (* matching_tokens *) diff -r d8c7be27e01d -r 8b0383334031 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Aug 08 19:36:31 2010 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Aug 08 19:54:54 2010 +0200 @@ -482,7 +482,7 @@ let val {lexicon, gram, parse_ast_trtab, ...} = tabs; val toks = Lexicon.tokenize lexicon xids syms; - val _ = List.app Lexicon.report_token toks; + val _ = List.app (Lexicon.report_token ctxt) toks; val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root; val pts = Parser.parse gram root' (filter Lexicon.is_proper toks); diff -r d8c7be27e01d -r 8b0383334031 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Sun Aug 08 19:36:31 2010 +0200 +++ b/src/Pure/context_position.ML Sun Aug 08 19:54:54 2010 +0200 @@ -9,7 +9,7 @@ val is_visible: Proof.context -> bool val set_visible: bool -> Proof.context -> Proof.context val restore_visible: Proof.context -> Proof.context -> Proof.context - val report_visible: Proof.context -> Markup.T -> Position.T -> unit + val report: Proof.context -> Markup.T -> Position.T -> unit end; structure Context_Position: CONTEXT_POSITION = @@ -25,7 +25,7 @@ val set_visible = Data.put; val restore_visible = set_visible o is_visible; -fun report_visible ctxt markup pos = +fun report ctxt markup pos = if is_visible ctxt then Position.report markup pos else (); end;