parse_sort/typ/term/prop: report markup;

--- a/src/Pure/Isar/proof_context.ML	Wed Aug 06 00:11:12 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 06 00:12:02 2008 +0200
@@ -639,28 +639,50 @@
 
 local
 
-fun parse_sort ctxt str =
-  Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str;
+fun parse_token markup text =
+  if YXML.detect text then
+    (case YXML.parse text of
+      XML.Elem ("token", props, [XML.Text str]) =>
+        let
+          val pos = Position.of_properties props;
+          val _ = Position.report markup pos;
+        in (translate_string (fn c => if c = Symbol.DEL then "" else c) str, pos) end
+    | _ => (text, Position.none))
+  else (text, Position.none);
 
-fun parse_typ ctxt str =
+fun parse_sort ctxt text =
+  let
+    val (str, pos) = parse_token Markup.sort text;
+    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (Sign.intern_sort (theory_of ctxt)) str
+      handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
+  in S end;
+
+fun parse_typ ctxt text =
   let
     val thy = ProofContext.theory_of ctxt;
     val get_sort = get_sort thy (Variable.def_sort ctxt);
+
+    val (str, pos) = parse_token Markup.typ text;
     val T = Sign.intern_tycons thy
-      (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str);
-  in T end
-  handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
+        (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) str)
+      handle ERROR msg => cat_error msg  ("Failed to parse type" ^ Position.str_of pos);
+  in T end;
 
-fun parse_term T ctxt str =
+fun parse_term T ctxt text =
   let
     val thy = theory_of ctxt;
+    val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
+
     val (T', _) = TypeInfer.paramify_dummies T 0;
+    val markup as (kind, _) = if T' = propT then Markup.proposition else Markup.term;
+    val (str, pos) = parse_token markup text;
+
     fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
-    val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
-    val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
-      map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T';
-  in read str end;
+    val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
+        map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' str
+      handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
+  in t end;
 
 
 fun unparse_sort ctxt S =