1.1 --- a/src/Pure/General/exn.ML Mon Apr 04 23:52:56 2011 +0200
1.2 +++ b/src/Pure/General/exn.ML Tue Apr 05 13:07:40 2011 +0200
1.3 @@ -11,7 +11,9 @@
1.4 val get_exn: 'a result -> exn option
1.5 val capture: ('a -> 'b) -> 'a -> 'b result
1.6 val release: 'a result -> 'a
1.7 + val flat_result: 'a result result -> 'a result
1.8 val map_result: ('a -> 'b) -> 'a result -> 'b result
1.9 + val maps_result: ('a -> 'b result) -> 'a result -> 'b result
1.10 exception Interrupt
1.11 val interrupt: unit -> 'a
1.12 val is_interrupt: exn -> bool
1.13 @@ -45,8 +47,13 @@
1.14 fun release (Result y) = y
1.15 | release (Exn e) = reraise e;
1.16
1.17 +fun flat_result (Result x) = x
1.18 + | flat_result (Exn e) = Exn e;
1.19 +
1.20 fun map_result f (Result x) = Result (f x)
1.21 - | map_result f (Exn e) = (Exn e);
1.22 + | map_result f (Exn e) = Exn e;
1.23 +
1.24 +fun maps_result f = flat_result o map_result f;
1.25
1.26
1.27 (* interrupts *)
2.1 --- a/src/Pure/Isar/proof_context.ML Mon Apr 04 23:52:56 2011 +0200
2.2 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 13:07:40 2011 +0200
2.3 @@ -67,7 +67,8 @@
2.4 val check_tfree: Proof.context -> string * sort -> string * sort
2.5 val type_context: Proof.context -> Syntax.type_context
2.6 val term_context: Proof.context -> Syntax.term_context
2.7 - val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
2.8 + val decode_term: Proof.context ->
2.9 + Position.reports * term Exn.result -> Position.reports * term Exn.result
2.10 val standard_infer_types: Proof.context -> term list -> term list
2.11 val read_term_pattern: Proof.context -> string -> term
2.12 val read_term_schematic: Proof.context -> string -> term
2.13 @@ -784,8 +785,8 @@
2.14 then default_root else c
2.15 | _ => default_root);
2.16
2.17 - fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
2.18 - handle ERROR msg => SOME msg;
2.19 + fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
2.20 + handle exn as ERROR _ => Exn.Exn exn;
2.21 val t =
2.22 Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
2.23 root (syms, pos)
3.1 --- a/src/Pure/Syntax/syn_trans.ML Mon Apr 04 23:52:56 2011 +0200
3.2 +++ b/src/Pure/Syntax/syn_trans.ML Tue Apr 05 13:07:40 2011 +0200
3.3 @@ -60,7 +60,7 @@
3.4 val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
3.5 val parsetree_to_ast: Proof.context -> type_context -> bool ->
3.6 (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
3.7 - Parser.parsetree -> Position.reports * Ast.ast
3.8 + Parser.parsetree -> Position.reports * Ast.ast Exn.result
3.9 val ast_to_term: Proof.context ->
3.10 (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
3.11 end;
3.12 @@ -587,7 +587,7 @@
3.13 | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
3.14 | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
3.15
3.16 - val ast = ast_of parsetree;
3.17 + val ast = Exn.interruptible_capture ast_of parsetree;
3.18 in (! reports, ast) end;
3.19
3.20
4.1 --- a/src/Pure/Syntax/syntax.ML Mon Apr 04 23:52:56 2011 +0200
4.2 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 13:07:40 2011 +0200
4.3 @@ -116,13 +116,13 @@
4.4 val ambiguity_level_raw: Config.raw
4.5 val ambiguity_level: int Config.T
4.6 val ambiguity_limit: int Config.T
4.7 - val standard_parse_term: (term -> string option) ->
4.8 + val standard_parse_sort: Proof.context -> type_context -> syntax ->
4.9 + Symbol_Pos.T list * Position.T -> sort
4.10 + val standard_parse_typ: Proof.context -> type_context -> syntax ->
4.11 + ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
4.12 + val standard_parse_term: (term -> term Exn.result) ->
4.13 Proof.context -> type_context -> term_context -> syntax ->
4.14 string -> Symbol_Pos.T list * Position.T -> term
4.15 - val standard_parse_typ: Proof.context -> type_context -> syntax ->
4.16 - ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
4.17 - val standard_parse_sort: Proof.context -> type_context -> syntax ->
4.18 - Symbol_Pos.T list * Position.T -> sort
4.19 datatype 'a trrule =
4.20 Parse_Rule of 'a * 'a |
4.21 Print_Rule of 'a * 'a |
4.22 @@ -130,13 +130,13 @@
4.23 val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
4.24 val is_const: syntax -> string -> bool
4.25 val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
4.26 + val standard_unparse_sort: {extern_class: string -> xstring} ->
4.27 + Proof.context -> syntax -> sort -> Pretty.T
4.28 + val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
4.29 + Proof.context -> syntax -> typ -> Pretty.T
4.30 val standard_unparse_term: {structs: string list, fixes: string list} ->
4.31 {extern_class: string -> xstring, extern_type: string -> xstring,
4.32 extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
4.33 - val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
4.34 - Proof.context -> syntax -> typ -> Pretty.T
4.35 - val standard_unparse_sort: {extern_class: string -> xstring} ->
4.36 - Proof.context -> syntax -> sort -> Pretty.T
4.37 val update_trfuns:
4.38 (string * ((ast list -> ast) * stamp)) list *
4.39 (string * ((term list -> term) * stamp)) list *
4.40 @@ -686,17 +686,9 @@
4.41
4.42
4.43
4.44 -(** read **)
4.45 +(** read **) (* FIXME rename!? *)
4.46
4.47 -fun some_results f xs =
4.48 - let
4.49 - val exn_results = map (Exn.interruptible_capture f) xs;
4.50 - val exns = map_filter Exn.get_exn exn_results;
4.51 - val results = map_filter Exn.get_result exn_results;
4.52 - in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
4.53 -
4.54 -
4.55 -(* read_ast *)
4.56 +(* configuration options *)
4.57
4.58 val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
4.59 val positions = Config.bool positions_raw;
4.60 @@ -712,6 +704,23 @@
4.61
4.62 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
4.63
4.64 +
4.65 +(* results *)
4.66 +
4.67 +fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
4.68 +fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
4.69 +
4.70 +fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
4.71 +
4.72 +fun report_result ctxt pos results =
4.73 + (case (proper_results results, failed_results results) of
4.74 + ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
4.75 + | ([(reports, x)], _) => (report ctxt reports; x)
4.76 + | _ => error (ambiguity_msg pos));
4.77 +
4.78 +
4.79 +(* read_asts *)
4.80 +
4.81 fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
4.82 let
4.83 val {lexicon, gram, parse_ast_trtab, ...} = tabs;
4.84 @@ -736,84 +745,87 @@
4.85 map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
4.86
4.87 val constrain_pos = not raw andalso Config.get ctxt positions;
4.88 + val parsetree_to_ast =
4.89 + Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab);
4.90 + in map parsetree_to_ast pts end;
4.91 +
4.92 +
4.93 +(* read_raw *)
4.94 +
4.95 +fun read_raw ctxt type_ctxt (syn as Syntax (tabs, _)) root input =
4.96 + let
4.97 + val {parse_ruletab, parse_trtab, ...} = tabs;
4.98 + val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
4.99 + val ast_to_term = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
4.100 in
4.101 - some_results
4.102 - (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
4.103 + read_asts ctxt type_ctxt syn false root input
4.104 + |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
4.105 end;
4.106
4.107
4.108 -(* read *)
4.109 +(* read sorts *)
4.110
4.111 -fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
4.112 - let val {parse_ruletab, parse_trtab, ...} = tabs in
4.113 - read_asts ctxt type_ctxt syn false root inp
4.114 - |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
4.115 - |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
4.116 - end;
4.117 -
4.118 -
4.119 -(* read terms *)
4.120 -
4.121 -fun report_result ctxt (reports, res) =
4.122 - (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
4.123 -
4.124 -(*brute-force disambiguation via type-inference*)
4.125 -fun disambig ctxt _ [arg] = report_result ctxt arg
4.126 - | disambig ctxt check args =
4.127 - let
4.128 - val level = Config.get ctxt ambiguity_level;
4.129 - val limit = Config.get ctxt ambiguity_limit;
4.130 -
4.131 - val ambiguity = length args;
4.132 - fun ambig_msg () =
4.133 - if ambiguity > 1 andalso ambiguity <= level then
4.134 - "Got more than one parse tree.\n\
4.135 - \Retry with smaller syntax_ambiguity_level for more information."
4.136 - else "";
4.137 -
4.138 - val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
4.139 - val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
4.140 - val len = length results;
4.141 -
4.142 - val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
4.143 - in
4.144 - if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
4.145 - else if len = 1 then
4.146 - (if ambiguity > level then
4.147 - Context_Position.if_visible ctxt warning
4.148 - "Fortunately, only one parse tree is type correct.\n\
4.149 - \You may still want to disambiguate your grammar or your input."
4.150 - else (); report_result ctxt (hd results))
4.151 - else cat_error (ambig_msg ()) (cat_lines
4.152 - (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
4.153 - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
4.154 - map (show_term o snd) (take limit results)))
4.155 - end;
4.156 -
4.157 -fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
4.158 - read ctxt type_ctxt syn root (syms, pos)
4.159 - |> map (Type_Ext.decode_term term_ctxt)
4.160 - |> disambig ctxt check;
4.161 +fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
4.162 + read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos)
4.163 + |> report_result ctxt pos
4.164 + |> Type_Ext.sort_of_term;
4.165
4.166
4.167 (* read types *)
4.168
4.169 fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
4.170 - (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
4.171 - [res] =>
4.172 - let val t = report_result ctxt res
4.173 - in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
4.174 - | _ => error (ambiguity_msg pos));
4.175 + read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos)
4.176 + |> report_result ctxt pos
4.177 + |> (fn t => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t);
4.178
4.179
4.180 -(* read sorts *)
4.181 +(* read terms -- brute-force disambiguation via type-inference *)
4.182
4.183 -fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
4.184 - (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
4.185 - [res] =>
4.186 - let val t = report_result ctxt res
4.187 - in Type_Ext.sort_of_term t end
4.188 - | _ => error (ambiguity_msg pos));
4.189 +fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
4.190 + let
4.191 + val results =
4.192 + read_raw ctxt type_ctxt syn root (syms, pos)
4.193 + |> map (Type_Ext.decode_term term_ctxt);
4.194 +
4.195 + val level = Config.get ctxt ambiguity_level;
4.196 + val limit = Config.get ctxt ambiguity_limit;
4.197 +
4.198 + val ambiguity = length (proper_results results);
4.199 +
4.200 + fun ambig_msg () =
4.201 + if ambiguity > 1 andalso ambiguity <= level then
4.202 + "Got more than one parse tree.\n\
4.203 + \Retry with smaller syntax_ambiguity_level for more information."
4.204 + else "";
4.205 +
4.206 + val results' =
4.207 + if ambiguity > 1 then
4.208 + (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
4.209 + else results;
4.210 + val reports' = fst (hd results');
4.211 +
4.212 + val errs = map snd (failed_results results');
4.213 + val checked = map snd (proper_results results');
4.214 + val len = length checked;
4.215 +
4.216 + val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
4.217 + in
4.218 + if len = 0 then
4.219 + report_result ctxt pos
4.220 + [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
4.221 + else if len = 1 then
4.222 + (if ambiguity > level then
4.223 + Context_Position.if_visible ctxt warning
4.224 + "Fortunately, only one parse tree is type correct.\n\
4.225 + \You may still want to disambiguate your grammar or your input."
4.226 + else (); report_result ctxt pos results')
4.227 + else
4.228 + report_result ctxt pos
4.229 + [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
4.230 + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
4.231 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
4.232 + map show_term (take limit checked))))))]
4.233 + end;
4.234
4.235
4.236
4.237 @@ -874,11 +886,9 @@
4.238
4.239 val (syms, pos) = read_token str;
4.240 in
4.241 - (case read_asts ctxt type_ctxt syn true root (syms, pos) of
4.242 - [res] =>
4.243 - let val ast = report_result ctxt res
4.244 - in constify ast end
4.245 - | _ => error (ambiguity_msg pos))
4.246 + read_asts ctxt type_ctxt syn true root (syms, pos)
4.247 + |> report_result ctxt pos
4.248 + |> constify
4.249 end;
4.250
4.251
4.252 @@ -899,16 +909,16 @@
4.253
4.254 in
4.255
4.256 -fun standard_unparse_term idents extern =
4.257 - unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
4.258 +fun standard_unparse_sort {extern_class} ctxt syn =
4.259 + unparse_t (K Printer.sort_to_ast)
4.260 + (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
4.261 + Markup.sort ctxt syn false;
4.262
4.263 fun standard_unparse_typ extern ctxt syn =
4.264 unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
4.265
4.266 -fun standard_unparse_sort {extern_class} ctxt syn =
4.267 - unparse_t (K Printer.sort_to_ast)
4.268 - (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
4.269 - Markup.sort ctxt syn false;
4.270 +fun standard_unparse_term idents extern =
4.271 + unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
4.272
4.273 end;
4.274
5.1 --- a/src/Pure/Syntax/type_ext.ML Mon Apr 04 23:52:56 2011 +0200
5.2 +++ b/src/Pure/Syntax/type_ext.ML Tue Apr 05 13:07:40 2011 +0200
5.3 @@ -13,7 +13,8 @@
5.4 val strip_positions: term -> term
5.5 val strip_positions_ast: Ast.ast -> Ast.ast
5.6 type term_context
5.7 - val decode_term: term_context -> Position.reports * term -> Position.reports * term
5.8 + val decode_term: term_context ->
5.9 + Position.reports * term Exn.result -> Position.reports * term Exn.result
5.10 val term_of_typ: bool -> typ -> term
5.11 val no_brackets: unit -> bool
5.12 val no_type_brackets: unit -> bool
5.13 @@ -136,55 +137,56 @@
5.14 markup_free: string -> Markup.T list,
5.15 markup_var: indexname -> Markup.T list};
5.16
5.17 -fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
5.18 - let
5.19 - val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
5.20 - val decodeT = typ_of_term (get_sort (term_sorts tm));
5.21 +fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
5.22 + | decode_term (term_context: term_context) (reports0, Exn.Result tm) =
5.23 + let
5.24 + val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
5.25 + val decodeT = typ_of_term (get_sort (term_sorts tm));
5.26
5.27 - val reports = Unsynchronized.ref reports0;
5.28 - fun report ps = Position.reports reports ps;
5.29 + val reports = Unsynchronized.ref reports0;
5.30 + fun report ps = Position.reports reports ps;
5.31
5.32 - fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
5.33 - (case decode_position typ of
5.34 - SOME p => decode (p :: ps) qs bs t
5.35 - | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
5.36 - | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
5.37 - (case decode_position typ of
5.38 - SOME q => decode ps (q :: qs) bs t
5.39 - | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
5.40 - | decode _ qs bs (Abs (x, T, t)) =
5.41 - let
5.42 - val id = serial_string ();
5.43 - val _ = report qs (markup_bound true) id;
5.44 - in Abs (x, T, decode [] [] (id :: bs) t) end
5.45 - | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
5.46 - | decode ps _ _ (Const (a, T)) =
5.47 - (case try Lexicon.unmark_fixed a of
5.48 - SOME x => (report ps markup_free x; Free (x, T))
5.49 - | NONE =>
5.50 + fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
5.51 + (case decode_position typ of
5.52 + SOME p => decode (p :: ps) qs bs t
5.53 + | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
5.54 + | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
5.55 + (case decode_position typ of
5.56 + SOME q => decode ps (q :: qs) bs t
5.57 + | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
5.58 + | decode _ qs bs (Abs (x, T, t)) =
5.59 let
5.60 - val c =
5.61 - (case try Lexicon.unmark_const a of
5.62 - SOME c => c
5.63 - | NONE => snd (get_const a));
5.64 - val _ = report ps markup_const c;
5.65 - in Const (c, T) end)
5.66 - | decode ps _ _ (Free (a, T)) =
5.67 - (case (get_free a, get_const a) of
5.68 - (SOME x, _) => (report ps markup_free x; Free (x, T))
5.69 - | (_, (true, c)) => (report ps markup_const c; Const (c, T))
5.70 - | (_, (false, c)) =>
5.71 - if Long_Name.is_qualified c
5.72 - then (report ps markup_const c; Const (c, T))
5.73 - else (report ps markup_free c; Free (c, T)))
5.74 - | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
5.75 - | decode ps _ bs (t as Bound i) =
5.76 - (case try (nth bs) i of
5.77 - SOME id => (report ps (markup_bound false) id; t)
5.78 - | NONE => t);
5.79 + val id = serial_string ();
5.80 + val _ = report qs (markup_bound true) id;
5.81 + in Abs (x, T, decode [] [] (id :: bs) t) end
5.82 + | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
5.83 + | decode ps _ _ (Const (a, T)) =
5.84 + (case try Lexicon.unmark_fixed a of
5.85 + SOME x => (report ps markup_free x; Free (x, T))
5.86 + | NONE =>
5.87 + let
5.88 + val c =
5.89 + (case try Lexicon.unmark_const a of
5.90 + SOME c => c
5.91 + | NONE => snd (get_const a));
5.92 + val _ = report ps markup_const c;
5.93 + in Const (c, T) end)
5.94 + | decode ps _ _ (Free (a, T)) =
5.95 + (case (get_free a, get_const a) of
5.96 + (SOME x, _) => (report ps markup_free x; Free (x, T))
5.97 + | (_, (true, c)) => (report ps markup_const c; Const (c, T))
5.98 + | (_, (false, c)) =>
5.99 + if Long_Name.is_qualified c
5.100 + then (report ps markup_const c; Const (c, T))
5.101 + else (report ps markup_free c; Free (c, T)))
5.102 + | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
5.103 + | decode ps _ bs (t as Bound i) =
5.104 + (case try (nth bs) i of
5.105 + SOME id => (report ps (markup_bound false) id; t)
5.106 + | NONE => t);
5.107
5.108 - val tm' = decode [] [] [] tm;
5.109 - in (! reports, tm') end;
5.110 + val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
5.111 + in (! reports, tm') end;
5.112
5.113
5.114