more precise propagation of reports/results through some inner syntax layers;
misc reorganization;

--- a/src/Pure/General/exn.ML	Mon Apr 04 23:52:56 2011 +0200
+++ b/src/Pure/General/exn.ML	Tue Apr 05 13:07:40 2011 +0200
@@ -11,7 +11,9 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
+  val flat_result: 'a result result -> 'a result
   val map_result: ('a -> 'b) -> 'a result -> 'b result
+  val maps_result: ('a -> 'b result) -> 'a result -> 'b result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
@@ -45,8 +47,13 @@
 fun release (Result y) = y
   | release (Exn e) = reraise e;
 
+fun flat_result (Result x) = x
+  | flat_result (Exn e) = Exn e;
+
 fun map_result f (Result x) = Result (f x)
-  | map_result f (Exn e) = (Exn e);
+  | map_result f (Exn e) = Exn e;
+
+fun maps_result f = flat_result o map_result f;
 
 
 (* interrupts *)

--- a/src/Pure/Isar/proof_context.ML	Mon Apr 04 23:52:56 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 05 13:07:40 2011 +0200
@@ -67,7 +67,8 @@
   val check_tfree: Proof.context -> string * sort -> string * sort
   val type_context: Proof.context -> Syntax.type_context
   val term_context: Proof.context -> Syntax.term_context
-  val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
+  val decode_term: Proof.context ->
+    Position.reports * term Exn.result -> Position.reports * term Exn.result
   val standard_infer_types: Proof.context -> term list -> term list
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
@@ -784,8 +785,8 @@
           then default_root else c
       | _ => default_root);
 
-    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
-      handle ERROR msg => SOME msg;
+    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
+      handle exn as ERROR _ => Exn.Exn exn;
     val t =
       Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
         root (syms, pos)

--- a/src/Pure/Syntax/syn_trans.ML	Mon Apr 04 23:52:56 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Apr 05 13:07:40 2011 +0200
@@ -60,7 +60,7 @@
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val parsetree_to_ast: Proof.context -> type_context -> bool ->
     (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
-    Parser.parsetree -> Position.reports * Ast.ast
+    Parser.parsetree -> Position.reports * Ast.ast Exn.result
   val ast_to_term: Proof.context ->
     (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
 end;
@@ -587,7 +587,7 @@
       | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
 
-    val ast = ast_of parsetree;
+    val ast = Exn.interruptible_capture ast_of parsetree;
   in (! reports, ast) end;
 
 

--- a/src/Pure/Syntax/syntax.ML	Mon Apr 04 23:52:56 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 05 13:07:40 2011 +0200
@@ -116,13 +116,13 @@
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
-  val standard_parse_term: (term -> string option) ->
+  val standard_parse_sort: Proof.context -> type_context -> syntax ->
+    Symbol_Pos.T list * Position.T -> sort
+  val standard_parse_typ: Proof.context -> type_context -> syntax ->
+    ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+  val standard_parse_term: (term -> term Exn.result) ->
     Proof.context -> type_context -> term_context -> syntax ->
     string -> Symbol_Pos.T list * Position.T -> term
-  val standard_parse_typ: Proof.context -> type_context -> syntax ->
-    ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
-  val standard_parse_sort: Proof.context -> type_context -> syntax ->
-    Symbol_Pos.T list * Position.T -> sort
   datatype 'a trrule =
     Parse_Rule of 'a * 'a |
     Print_Rule of 'a * 'a |
@@ -130,13 +130,13 @@
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val is_const: syntax -> string -> bool
   val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
+  val standard_unparse_sort: {extern_class: string -> xstring} ->
+    Proof.context -> syntax -> sort -> Pretty.T
+  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+    Proof.context -> syntax -> typ -> Pretty.T
   val standard_unparse_term: {structs: string list, fixes: string list} ->
     {extern_class: string -> xstring, extern_type: string -> xstring,
       extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
-  val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
-    Proof.context -> syntax -> typ -> Pretty.T
-  val standard_unparse_sort: {extern_class: string -> xstring} ->
-    Proof.context -> syntax -> sort -> Pretty.T
   val update_trfuns:
     (string * ((ast list -> ast) * stamp)) list *
     (string * ((term list -> term) * stamp)) list *
@@ -686,17 +686,9 @@
 
 
 
-(** read **)
+(** read **)  (* FIXME rename!? *)
 
-fun some_results f xs =
-  let
-    val exn_results = map (Exn.interruptible_capture f) xs;
-    val exns = map_filter Exn.get_exn exn_results;
-    val results = map_filter Exn.get_result exn_results;
-  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
-
-
-(* read_ast *)
+(* configuration options *)
 
 val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
 val positions = Config.bool positions_raw;
@@ -712,6 +704,23 @@
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
+
+(* results *)
+
+fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
+
+fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
+
+fun report_result ctxt pos results =
+  (case (proper_results results, failed_results results) of
+    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
+  | ([(reports, x)], _) => (report ctxt reports; x)
+  | _ => error (ambiguity_msg pos));
+
+
+(* read_asts *)
+
 fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
@@ -736,84 +745,87 @@
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
 
     val constrain_pos = not raw andalso Config.get ctxt positions;
-  in
-    some_results
-      (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
-  end;
+    val parsetree_to_ast =
+      Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab);
+  in map parsetree_to_ast pts end;
 
 
-(* read *)
+(* read_raw *)
 
-fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
-  let val {parse_ruletab, parse_trtab, ...} = tabs in
-    read_asts ctxt type_ctxt syn false root inp
-    |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
-    |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
+fun read_raw ctxt type_ctxt (syn as Syntax (tabs, _)) root input =
+  let
+    val {parse_ruletab, parse_trtab, ...} = tabs;
+    val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
+    val ast_to_term = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
+  in
+    read_asts ctxt type_ctxt syn false root input
+    |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
   end;
 
 
-(* read terms *)
-
-fun report_result ctxt (reports, res) =
-  (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
-
-(*brute-force disambiguation via type-inference*)
-fun disambig ctxt _ [arg] = report_result ctxt arg
-  | disambig ctxt check args =
-      let
-        val level = Config.get ctxt ambiguity_level;
-        val limit = Config.get ctxt ambiguity_limit;
-
-        val ambiguity = length args;
-        fun ambig_msg () =
-          if ambiguity > 1 andalso ambiguity <= level then
-            "Got more than one parse tree.\n\
-            \Retry with smaller syntax_ambiguity_level for more information."
-          else "";
+(* read sorts *)
 
-        val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
-        val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
-        val len = length results;
-
-        val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
-      in
-        if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
-        else if len = 1 then
-          (if ambiguity > level then
-            Context_Position.if_visible ctxt warning
-              "Fortunately, only one parse tree is type correct.\n\
-              \You may still want to disambiguate your grammar or your input."
-          else (); report_result ctxt (hd results))
-        else cat_error (ambig_msg ()) (cat_lines
-          (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
-            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (show_term o snd) (take limit results)))
-      end;
-
-fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
-  read ctxt type_ctxt syn root (syms, pos)
-  |> map (Type_Ext.decode_term term_ctxt)
-  |> disambig ctxt check;
+fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
+  read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos)
+  |> report_result ctxt pos
+  |> Type_Ext.sort_of_term;
 
 
 (* read types *)
 
 fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
-  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
-    [res] =>
-      let val t = report_result ctxt res
-      in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
-  | _ => error (ambiguity_msg pos));
+  read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos)
+  |> report_result ctxt pos
+  |> (fn t => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t);
 
 
-(* read sorts *)
+(* read terms -- brute-force disambiguation via type-inference *)
+
+fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
+  let
+    val results =
+      read_raw ctxt type_ctxt syn root (syms, pos)
+      |> map (Type_Ext.decode_term term_ctxt);
+
+    val level = Config.get ctxt ambiguity_level;
+    val limit = Config.get ctxt ambiguity_limit;
+
+    val ambiguity = length (proper_results results);
+
+    fun ambig_msg () =
+      if ambiguity > 1 andalso ambiguity <= level then
+        "Got more than one parse tree.\n\
+        \Retry with smaller syntax_ambiguity_level for more information."
+      else "";
 
-fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
-  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
-    [res] =>
-      let val t = report_result ctxt res
-      in Type_Ext.sort_of_term t end
-  | _ => error (ambiguity_msg pos));
+    val results' =
+      if ambiguity > 1 then
+        (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
+      else results;
+    val reports' = fst (hd results');
+
+    val errs = map snd (failed_results results');
+    val checked = map snd (proper_results results');
+    val len = length checked;
+
+    val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
+  in
+    if len = 0 then
+      report_result ctxt pos
+        [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
+    else if len = 1 then
+      (if ambiguity > level then
+        Context_Position.if_visible ctxt warning
+          "Fortunately, only one parse tree is type correct.\n\
+          \You may still want to disambiguate your grammar or your input."
+      else (); report_result ctxt pos results')
+    else
+      report_result ctxt pos
+        [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
+          (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
+            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+            map show_term (take limit checked))))))]
+  end;
 
 
 
@@ -874,11 +886,9 @@
 
     val (syms, pos) = read_token str;
   in
-    (case read_asts ctxt type_ctxt syn true root (syms, pos) of
-      [res] =>
-        let val ast = report_result ctxt res
-        in constify ast end
-    | _ => error (ambiguity_msg pos))
+    read_asts ctxt type_ctxt syn true root (syms, pos)
+    |> report_result ctxt pos
+    |> constify
   end;
 
 
@@ -899,16 +909,16 @@
 
 in
 
-fun standard_unparse_term idents extern =
-  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_sort {extern_class} ctxt syn =
+  unparse_t (K Printer.sort_to_ast)
+    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+    Markup.sort ctxt syn false;
 
 fun standard_unparse_typ extern ctxt syn =
   unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
 
-fun standard_unparse_sort {extern_class} ctxt syn =
-  unparse_t (K Printer.sort_to_ast)
-    (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
-    Markup.sort ctxt syn false;
+fun standard_unparse_term idents extern =
+  unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
 
 end;
 

--- a/src/Pure/Syntax/type_ext.ML	Mon Apr 04 23:52:56 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Tue Apr 05 13:07:40 2011 +0200
@@ -13,7 +13,8 @@
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
   type term_context
-  val decode_term: term_context -> Position.reports * term -> Position.reports * term
+  val decode_term: term_context ->
+    Position.reports * term Exn.result -> Position.reports * term Exn.result
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
@@ -136,55 +137,56 @@
   markup_free: string -> Markup.T list,
   markup_var: indexname -> Markup.T list};
 
-fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
-  let
-    val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
-    val decodeT = typ_of_term (get_sort (term_sorts tm));
+fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+  | decode_term (term_context: term_context) (reports0, Exn.Result tm) =
+      let
+        val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
+        val decodeT = typ_of_term (get_sort (term_sorts tm));
 
-    val reports = Unsynchronized.ref reports0;
-    fun report ps = Position.reports reports ps;
+        val reports = Unsynchronized.ref reports0;
+        fun report ps = Position.reports reports ps;
 
-    fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
-          (case decode_position typ of
-            SOME p => decode (p :: ps) qs bs t
-          | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
-      | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
-          (case decode_position typ of
-            SOME q => decode ps (q :: qs) bs t
-          | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
-      | decode _ qs bs (Abs (x, T, t)) =
-          let
-            val id = serial_string ();
-            val _ = report qs (markup_bound true) id;
-          in Abs (x, T, decode [] [] (id :: bs) t) end
-      | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
-      | decode ps _ _ (Const (a, T)) =
-          (case try Lexicon.unmark_fixed a of
-            SOME x => (report ps markup_free x; Free (x, T))
-          | NONE =>
+        fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
+              (case decode_position typ of
+                SOME p => decode (p :: ps) qs bs t
+              | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
+          | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
+              (case decode_position typ of
+                SOME q => decode ps (q :: qs) bs t
+              | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
+          | decode _ qs bs (Abs (x, T, t)) =
               let
-                val c =
-                  (case try Lexicon.unmark_const a of
-                    SOME c => c
-                  | NONE => snd (get_const a));
-                val _ = report ps markup_const c;
-              in Const (c, T) end)
-      | decode ps _ _ (Free (a, T)) =
-          (case (get_free a, get_const a) of
-            (SOME x, _) => (report ps markup_free x; Free (x, T))
-          | (_, (true, c)) => (report ps markup_const c; Const (c, T))
-          | (_, (false, c)) =>
-              if Long_Name.is_qualified c
-              then (report ps markup_const c; Const (c, T))
-              else (report ps markup_free c; Free (c, T)))
-      | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
-      | decode ps _ bs (t as Bound i) =
-          (case try (nth bs) i of
-            SOME id => (report ps (markup_bound false) id; t)
-          | NONE => t);
+                val id = serial_string ();
+                val _ = report qs (markup_bound true) id;
+              in Abs (x, T, decode [] [] (id :: bs) t) end
+          | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
+          | decode ps _ _ (Const (a, T)) =
+              (case try Lexicon.unmark_fixed a of
+                SOME x => (report ps markup_free x; Free (x, T))
+              | NONE =>
+                  let
+                    val c =
+                      (case try Lexicon.unmark_const a of
+                        SOME c => c
+                      | NONE => snd (get_const a));
+                    val _ = report ps markup_const c;
+                  in Const (c, T) end)
+          | decode ps _ _ (Free (a, T)) =
+              (case (get_free a, get_const a) of
+                (SOME x, _) => (report ps markup_free x; Free (x, T))
+              | (_, (true, c)) => (report ps markup_const c; Const (c, T))
+              | (_, (false, c)) =>
+                  if Long_Name.is_qualified c
+                  then (report ps markup_const c; Const (c, T))
+                  else (report ps markup_free c; Free (c, T)))
+          | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
+          | decode ps _ bs (t as Bound i) =
+              (case try (nth bs) i of
+                SOME id => (report ps (markup_bound false) id; t)
+              | NONE => t);
 
-    val tm' = decode [] [] [] tm;
-  in (! reports, tm') end;
+        val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+      in (! reports, tm') end;