src/Pure/Syntax/syntax.ML
changeset 28407 f9db1da584ac
parent 28375 c879d88d038a
child 28413 ee73353fb87c
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:24 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:41:25 2008 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4      (string * string) trrule list -> syntax -> syntax
     1.5    val update_trrules_i: ast trrule list -> syntax -> syntax
     1.6    val remove_trrules_i: ast trrule list -> syntax -> syntax
     1.7 -  val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
     1.8 +  val parse_token: Proof.context -> Markup.T -> string -> SymbolPos.T list * Position.T
     1.9    val parse_sort: Proof.context -> string -> sort
    1.10    val parse_typ: Proof.context -> string -> typ
    1.11    val parse_term: Proof.context -> string -> term
    1.12 @@ -482,7 +482,7 @@
    1.13    let
    1.14      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    1.15      val toks = Lexicon.tokenize lexicon xids syms;
    1.16 -    val _ = List.app Lexicon.report_token toks;
    1.17 +    val _ = List.app (Lexicon.report_token ctxt) toks;
    1.18  
    1.19      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    1.20      val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
    1.21 @@ -695,10 +695,10 @@
    1.22  
    1.23  (* (un)parsing *)
    1.24  
    1.25 -fun parse_token markup str =
    1.26 +fun parse_token ctxt markup str =
    1.27    let
    1.28      val (syms, pos) = read_token str;
    1.29 -    val _ = Position.report markup pos;
    1.30 +    val _ = ContextPosition.report ctxt markup pos;
    1.31    in (syms, pos) end;
    1.32  
    1.33  local