src/Pure/Isar/proof_context.ML
changeset 27785 3bf65bfda540
parent 27754 36df922b82d4
child 27821 0ead8c2428f9
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 07 21:13:01 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 07 22:32:01 2008 +0200
     1.3 @@ -639,21 +639,17 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun parse_token markup text =
     1.8 -  if YXML.detect text then
     1.9 -    (case YXML.parse text of
    1.10 -      XML.Elem ("token", props, [XML.Text str]) =>
    1.11 -        let
    1.12 -          val pos = Position.of_properties props;
    1.13 -          val _ = Position.report markup pos;
    1.14 -        in (translate_string (fn c => if c = Symbol.DEL then "" else c) str, pos) end
    1.15 -    | _ => (text, Position.none))
    1.16 -  else (text, Position.none);
    1.17 +fun parse_token markup str =
    1.18 +  let
    1.19 +    val (syms, pos) = Syntax.read_token str;
    1.20 +    val _ = Position.report markup pos;
    1.21 +  in (syms, pos) end;
    1.22  
    1.23  fun parse_sort ctxt text =
    1.24    let
    1.25 -    val (str, pos) = parse_token Markup.sort text;
    1.26 -    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str
    1.27 +    val (syms, pos) = parse_token Markup.sort text;
    1.28 +    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
    1.29 +        (Sign.intern_sort (theory_of ctxt)) (syms, pos)
    1.30        handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    1.31    in S end;
    1.32  
    1.33 @@ -662,9 +658,9 @@
    1.34      val thy = ProofContext.theory_of ctxt;
    1.35      val get_sort = get_sort thy (Variable.def_sort ctxt);
    1.36  
    1.37 -    val (str, pos) = parse_token Markup.typ text;
    1.38 +    val (syms, pos) = parse_token Markup.typ text;
    1.39      val T = Sign.intern_tycons thy
    1.40 -        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str)
    1.41 +        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
    1.42        handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
    1.43    in T end;
    1.44  
    1.45 @@ -675,12 +671,12 @@
    1.46  
    1.47      val (T', _) = TypeInfer.paramify_dummies T 0;
    1.48      val markup as (kind, _) = if T' = propT then Markup.proposition else Markup.term;
    1.49 -    val (str, pos) = parse_token markup text;
    1.50 +    val (syms, pos) = parse_token markup text;
    1.51  
    1.52      fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
    1.53        handle ERROR msg => SOME msg;
    1.54 -    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
    1.55 -        map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' str
    1.56 +    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    1.57 +        map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
    1.58        handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
    1.59    in t end;
    1.60