report_token/parse_token: back to context-less version;
authorwenzelm
Mon Sep 29 21:26:41 2008 +0200 (2008-09-29)
changeset 28413ee73353fb87c
parent 28412 0608c04858c7
child 28414 419954d26886
report_token/parse_token: back to context-less version;
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Sep 29 21:26:39 2008 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 29 21:26:41 2008 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val tvarT: typ
     1.5    val terminals: string list
     1.6    val is_terminal: string -> bool
     1.7 -  val report_token: Proof.context -> token -> unit
     1.8 +  val report_token: token -> unit
     1.9    val matching_tokens: token * token -> bool
    1.10    val valued_token: token -> bool
    1.11    val predef_term: string -> token option
    1.12 @@ -162,8 +162,8 @@
    1.13    | Comment     => Markup.inner_comment
    1.14    | EOF         => Markup.none;
    1.15  
    1.16 -fun report_token ctxt (Token (kind, _, (pos, _))) =
    1.17 -  ContextPosition.report ctxt (token_kind_markup kind) pos;
    1.18 +fun report_token (Token (kind, _, (pos, _))) =
    1.19 +  Position.report (token_kind_markup kind) pos;
    1.20  
    1.21  
    1.22  (* matching_tokens *)
     2.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 21:26:39 2008 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 21:26:41 2008 +0200
     2.3 @@ -83,7 +83,7 @@
     2.4      (string * string) trrule list -> syntax -> syntax
     2.5    val update_trrules_i: ast trrule list -> syntax -> syntax
     2.6    val remove_trrules_i: ast trrule list -> syntax -> syntax
     2.7 -  val parse_token: Proof.context -> Markup.T -> string -> SymbolPos.T list * Position.T
     2.8 +  val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
     2.9    val parse_sort: Proof.context -> string -> sort
    2.10    val parse_typ: Proof.context -> string -> typ
    2.11    val parse_term: Proof.context -> string -> term
    2.12 @@ -482,7 +482,7 @@
    2.13    let
    2.14      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    2.15      val toks = Lexicon.tokenize lexicon xids syms;
    2.16 -    val _ = List.app (Lexicon.report_token ctxt) toks;
    2.17 +    val _ = List.app Lexicon.report_token toks;
    2.18  
    2.19      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    2.20      val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
    2.21 @@ -695,10 +695,10 @@
    2.22  
    2.23  (* (un)parsing *)
    2.24  
    2.25 -fun parse_token ctxt markup str =
    2.26 +fun parse_token markup str =
    2.27    let
    2.28      val (syms, pos) = read_token str;
    2.29 -    val _ = ContextPosition.report ctxt markup pos;
    2.30 +    val _ = Position.report markup pos;
    2.31    in (syms, pos) end;
    2.32  
    2.33  local