# HG changeset patch # User wenzelm # Date 1222716401 -7200 # Node ID ee73353fb87ce3290b694667d007890b8120300a # Parent 0608c04858c74d31e4a11ef08ff6c009a4e72166 report_token/parse_token: back to context-less version; diff -r 0608c04858c7 -r ee73353fb87c src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon Sep 29 21:26:39 2008 +0200 +++ b/src/Pure/Syntax/lexicon.ML Mon Sep 29 21:26:41 2008 +0200 @@ -56,7 +56,7 @@ val tvarT: typ val terminals: string list val is_terminal: string -> bool - val report_token: Proof.context -> token -> unit + val report_token: token -> unit val matching_tokens: token * token -> bool val valued_token: token -> bool val predef_term: string -> token option @@ -162,8 +162,8 @@ | Comment => Markup.inner_comment | EOF => Markup.none; -fun report_token ctxt (Token (kind, _, (pos, _))) = - ContextPosition.report ctxt (token_kind_markup kind) pos; +fun report_token (Token (kind, _, (pos, _))) = + Position.report (token_kind_markup kind) pos; (* matching_tokens *) diff -r 0608c04858c7 -r ee73353fb87c src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Sep 29 21:26:39 2008 +0200 +++ b/src/Pure/Syntax/syntax.ML Mon Sep 29 21:26:41 2008 +0200 @@ -83,7 +83,7 @@ (string * string) trrule list -> syntax -> syntax val update_trrules_i: ast trrule list -> syntax -> syntax val remove_trrules_i: ast trrule list -> syntax -> syntax - val parse_token: Proof.context -> Markup.T -> string -> SymbolPos.T list * Position.T + val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ val parse_term: Proof.context -> string -> term @@ -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 ctxt) toks; + val _ = List.app Lexicon.report_token toks; val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root; val pts = Parser.parse gram root' (filter Lexicon.is_proper toks); @@ -695,10 +695,10 @@ (* (un)parsing *) -fun parse_token ctxt markup str = +fun parse_token markup str = let val (syms, pos) = read_token str; - val _ = ContextPosition.report ctxt markup pos; + val _ = Position.report markup pos; in (syms, pos) end; local