src/Pure/Syntax/type_ext.ML

--- 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;