src/Pure/Syntax/syntax.ML
changeset 27822 a6319699e517
parent 27808 4dd3d5efcc7f
child 27889 c9e8a5bda32b
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Aug 10 12:38:25 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Aug 10 12:38:26 2008 +0200
     1.3 @@ -83,6 +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_sort: Proof.context -> string -> sort
     1.9    val parse_typ: Proof.context -> string -> typ
    1.10    val parse_term: Proof.context -> string -> term
    1.11 @@ -694,6 +695,12 @@
    1.12  
    1.13  (* (un)parsing *)
    1.14  
    1.15 +fun parse_token markup str =
    1.16 +  let
    1.17 +    val (syms, pos) = read_token str;
    1.18 +    val _ = Position.report markup pos;
    1.19 +  in (syms, pos) end;
    1.20 +
    1.21  local
    1.22    type operations =
    1.23     {parse_sort: Proof.context -> string -> sort,