parse_sort/typ/term/prop: report markup;
authorwenzelm
Wed Aug 06 00:12:02 2008 +0200 (2008-08-06 ago)
changeset 2775436df922b82d4
parent 27753 94b672153b49
child 27755 f7cdde18aeb3
parse_sort/typ/term/prop: report markup;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 06 00:11:12 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 06 00:12:02 2008 +0200
     1.3 @@ -639,28 +639,50 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun parse_sort ctxt str =
     1.8 -  Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str;
     1.9 +fun parse_token markup text =
    1.10 +  if YXML.detect text then
    1.11 +    (case YXML.parse text of
    1.12 +      XML.Elem ("token", props, [XML.Text str]) =>
    1.13 +        let
    1.14 +          val pos = Position.of_properties props;
    1.15 +          val _ = Position.report markup pos;
    1.16 +        in (translate_string (fn c => if c = Symbol.DEL then "" else c) str, pos) end
    1.17 +    | _ => (text, Position.none))
    1.18 +  else (text, Position.none);
    1.19  
    1.20 -fun parse_typ ctxt str =
    1.21 +fun parse_sort ctxt text =
    1.22 +  let
    1.23 +    val (str, pos) = parse_token Markup.sort text;
    1.24 +    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str
    1.25 +      handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
    1.26 +  in S end;
    1.27 +
    1.28 +fun parse_typ ctxt text =
    1.29    let
    1.30      val thy = ProofContext.theory_of ctxt;
    1.31      val get_sort = get_sort thy (Variable.def_sort ctxt);
    1.32 +
    1.33 +    val (str, pos) = parse_token Markup.typ text;
    1.34      val T = Sign.intern_tycons thy
    1.35 -      (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str);
    1.36 -  in T end
    1.37 -  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
    1.38 +        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str)
    1.39 +      handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
    1.40 +  in T end;
    1.41  
    1.42 -fun parse_term T ctxt str =
    1.43 +fun parse_term T ctxt text =
    1.44    let
    1.45      val thy = theory_of ctxt;
    1.46 +    val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
    1.47 +
    1.48      val (T', _) = TypeInfer.paramify_dummies T 0;
    1.49 +    val markup as (kind, _) = if T' = propT then Markup.proposition else Markup.term;
    1.50 +    val (str, 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 {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
    1.55 -    val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
    1.56 -      map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T';
    1.57 -  in read str end;
    1.58 +    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
    1.59 +        map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' str
    1.60 +      handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
    1.61 +  in t end;
    1.62  
    1.63  
    1.64  fun unparse_sort ctxt S =