1.1 --- a/src/Pure/Concurrent/future.ML Mon Jul 11 18:44:58 2011 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Mon Jul 11 23:20:40 2011 +0200
1.3 @@ -117,7 +117,7 @@
1.4 val ok =
1.5 (case the (Single_Assignment.peek result) of
1.6 Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
1.7 - | Exn.Result _ => true);
1.8 + | Exn.Res _ => true);
1.9 in ok end;
1.10
1.11
1.12 @@ -482,7 +482,7 @@
1.13 val task = Task_Queue.dummy_task ();
1.14 val group = Task_Queue.group_of_task task;
1.15 val result = Single_Assignment.var "value" : 'a result;
1.16 - val _ = assign_result group result (Exn.Result x);
1.17 + val _ = assign_result group result (Exn.Res x);
1.18 in Future {promised = false, task = task, result = result} end;
1.19
1.20 fun map_future f x =
1.21 @@ -544,7 +544,7 @@
1.22 else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
1.23 in () end;
1.24
1.25 -fun fulfill x res = fulfill_result x (Exn.Result res);
1.26 +fun fulfill x res = fulfill_result x (Exn.Res res);
1.27
1.28
1.29 (* cancellation *)
2.1 --- a/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 18:44:58 2011 +0200
2.2 +++ b/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 23:20:40 2011 +0200
2.3 @@ -23,7 +23,7 @@
2.4 | Result res => SOME res);
2.5
2.6 fun lazy e = Lazy (Unsynchronized.ref (Expr e));
2.7 -fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
2.8 +fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
2.9
2.10
2.11 (* force result *)
3.1 --- a/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 18:44:58 2011 +0200
3.2 +++ b/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 23:20:40 2011 +0200
3.3 @@ -38,7 +38,7 @@
3.4 (case peek v of
3.5 NONE =>
3.6 (case Multithreading.sync_wait NONE NONE cond lock of
3.7 - Exn.Result _ => wait ()
3.8 + Exn.Res _ => wait ()
3.9 | Exn.Exn exn => reraise exn)
3.10 | SOME x => x);
3.11 in wait () end);
4.1 --- a/src/Pure/Concurrent/synchronized.ML Mon Jul 11 18:44:58 2011 +0200
4.2 +++ b/src/Pure/Concurrent/synchronized.ML Mon Jul 11 23:20:40 2011 +0200
4.3 @@ -47,8 +47,8 @@
4.4 (case f x of
4.5 NONE =>
4.6 (case Multithreading.sync_wait NONE (time_limit x) cond lock of
4.7 - Exn.Result true => try_change ()
4.8 - | Exn.Result false => NONE
4.9 + Exn.Res true => try_change ()
4.10 + | Exn.Res false => NONE
4.11 | Exn.Exn exn => reraise exn)
4.12 | SOME (y, x') =>
4.13 uninterruptible (fn _ => fn () =>
5.1 --- a/src/Pure/General/exn.ML Mon Jul 11 18:44:58 2011 +0200
5.2 +++ b/src/Pure/General/exn.ML Mon Jul 11 23:20:40 2011 +0200
5.3 @@ -1,13 +1,13 @@
5.4 (* Title: Pure/General/exn.ML
5.5 Author: Makarius
5.6
5.7 -Extra support for exceptions.
5.8 +Support for exceptions.
5.9 *)
5.10
5.11 signature EXN =
5.12 sig
5.13 - datatype 'a result = Result of 'a | Exn of exn
5.14 - val get_result: 'a result -> 'a option
5.15 + datatype 'a result = Res of 'a | Exn of exn
5.16 + val get_res: 'a result -> 'a option
5.17 val get_exn: 'a result -> exn option
5.18 val capture: ('a -> 'b) -> 'a -> 'b result
5.19 val release: 'a result -> 'a
5.20 @@ -33,24 +33,24 @@
5.21 (* runtime exceptions as values *)
5.22
5.23 datatype 'a result =
5.24 - Result of 'a |
5.25 + Res of 'a |
5.26 Exn of exn;
5.27
5.28 -fun get_result (Result x) = SOME x
5.29 - | get_result _ = NONE;
5.30 +fun get_res (Res x) = SOME x
5.31 + | get_res _ = NONE;
5.32
5.33 fun get_exn (Exn exn) = SOME exn
5.34 | get_exn _ = NONE;
5.35
5.36 -fun capture f x = Result (f x) handle e => Exn e;
5.37 +fun capture f x = Res (f x) handle e => Exn e;
5.38
5.39 -fun release (Result y) = y
5.40 +fun release (Res y) = y
5.41 | release (Exn e) = reraise e;
5.42
5.43 -fun flat_result (Result x) = x
5.44 +fun flat_result (Res x) = x
5.45 | flat_result (Exn e) = Exn e;
5.46
5.47 -fun map_result f (Result x) = Result (f x)
5.48 +fun map_result f (Res x) = Res (f x)
5.49 | map_result f (Exn e) = Exn e;
5.50
5.51 fun maps_result f = flat_result o map_result f;
5.52 @@ -72,7 +72,7 @@
5.53 | is_interrupt_exn _ = false;
5.54
5.55 fun interruptible_capture f x =
5.56 - Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
5.57 + Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
5.58
5.59
5.60 (* nested exceptions *)
5.61 @@ -84,8 +84,8 @@
5.62 and flatten_list exns = List.concat (map flatten exns);
5.63
5.64 fun release_all results =
5.65 - if List.all (fn Result _ => true | _ => false) results
5.66 - then map (fn Result x => x) results
5.67 + if List.all (fn Res _ => true | _ => false) results
5.68 + then map (fn Res x => x) results
5.69 else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
5.70
5.71 fun release_first results = release_all results
6.1 --- a/src/Pure/General/exn.scala Mon Jul 11 18:44:58 2011 +0200
6.2 +++ b/src/Pure/General/exn.scala Mon Jul 11 23:20:40 2011 +0200
6.3 @@ -1,7 +1,7 @@
6.4 /* Title: Pure/General/exn.scala
6.5 Author: Makarius
6.6
6.7 -Extra support for exceptions (arbitrary throwables).
6.8 +Support for exceptions (arbitrary throwables).
6.9 */
6.10
6.11 package isabelle
6.12 @@ -12,8 +12,8 @@
6.13 /* runtime exceptions as values */
6.14
6.15 sealed abstract class Result[A]
6.16 - case class Res[A](val result: A) extends Result[A]
6.17 - case class Exn[A](val exn: Throwable) extends Result[A]
6.18 + case class Res[A](res: A) extends Result[A]
6.19 + case class Exn[A](exn: Throwable) extends Result[A]
6.20
6.21 def capture[A](e: => A): Result[A] =
6.22 try { Res(e) }
7.1 --- a/src/Pure/General/output.ML Mon Jul 11 18:44:58 2011 +0200
7.2 +++ b/src/Pure/General/output.ML Mon Jul 11 23:20:40 2011 +0200
7.3 @@ -96,9 +96,8 @@
7.4 val prompt_fn = Unsynchronized.ref raw_stdout;
7.5 val status_fn = Unsynchronized.ref (fn _: output => ());
7.6 val report_fn = Unsynchronized.ref (fn _: output => ());
7.7 - val raw_message_fn =
7.8 - Unsynchronized.ref
7.9 - (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
7.10 + val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
7.11 + Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
7.12 end;
7.13
7.14 fun writeln s = ! Private_Hooks.writeln_fn (output s);
8.1 --- a/src/Pure/Isar/proof.ML Mon Jul 11 18:44:58 2011 +0200
8.2 +++ b/src/Pure/Isar/proof.ML Mon Jul 11 23:20:40 2011 +0200
8.3 @@ -1008,8 +1008,8 @@
8.4 |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
8.5 |> int ? (fn goal_state =>
8.6 (case test_proof goal_state of
8.7 - Exn.Result (SOME _) => goal_state
8.8 - | Exn.Result NONE => error (fail_msg (context_of goal_state))
8.9 + Exn.Res (SOME _) => goal_state
8.10 + | Exn.Res NONE => error (fail_msg (context_of goal_state))
8.11 | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
8.12 end;
8.13
9.1 --- a/src/Pure/Isar/runtime.ML Mon Jul 11 18:44:58 2011 +0200
9.2 +++ b/src/Pure/Isar/runtime.ML Mon Jul 11 23:20:40 2011 +0200
9.3 @@ -101,7 +101,7 @@
9.4 fun debugging f x =
9.5 if ! debug then
9.6 Exn.release (exception_trace (fn () =>
9.7 - Exn.Result (f x) handle
9.8 + Exn.Res (f x) handle
9.9 exn as UNDEF => Exn.Exn exn
9.10 | exn as EXCURSION_FAIL _ => Exn.Exn exn))
9.11 else f x;
10.1 --- a/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 18:44:58 2011 +0200
10.2 +++ b/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 23:20:40 2011 +0200
10.3 @@ -55,7 +55,7 @@
10.4
10.5 fun with_attributes _ e = e [];
10.6
10.7 -fun sync_wait _ _ _ _ = Exn.Result true;
10.8 +fun sync_wait _ _ _ _ = Exn.Res true;
10.9
10.10
10.11 (* tracing *)
11.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 18:44:58 2011 +0200
11.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 23:20:40 2011 +0200
11.3 @@ -97,8 +97,8 @@
11.4 (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
11.5 (fn _ =>
11.6 (case time of
11.7 - SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
11.8 - | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
11.9 + SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
11.10 + | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
11.11 handle exn => Exn.Exn exn);
11.12
11.13
12.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 18:44:58 2011 +0200
12.2 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 23:20:40 2011 +0200
12.3 @@ -14,13 +14,13 @@
12.4 (case Future.peek x of
12.5 NONE => PolyML.PrettyString "<future>"
12.6 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
12.7 - | SOME (Exn.Result y) => pretty (y, depth)));
12.8 + | SOME (Exn.Res y) => pretty (y, depth)));
12.9
12.10 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
12.11 (case Lazy.peek x of
12.12 NONE => PolyML.PrettyString "<lazy>"
12.13 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
12.14 - | SOME (Exn.Result y) => pretty (y, depth)));
12.15 + | SOME (Exn.Res y) => pretty (y, depth)));
12.16
12.17 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
12.18 let
13.1 --- a/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 18:44:58 2011 +0200
13.2 +++ b/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 23:20:40 2011 +0200
13.3 @@ -9,12 +9,12 @@
13.4 (case Future.peek x of
13.5 NONE => str "<future>"
13.6 | SOME (Exn.Exn _) => str "<failed>"
13.7 - | SOME (Exn.Result y) => print (y, depth)));
13.8 + | SOME (Exn.Res y) => print (y, depth)));
13.9
13.10 PolyML.install_pp
13.11 (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
13.12 (case Lazy.peek x of
13.13 NONE => str "<lazy>"
13.14 | SOME (Exn.Exn _) => str "<failed>"
13.15 - | SOME (Exn.Result y) => print (y, depth)));
13.16 + | SOME (Exn.Res y) => print (y, depth)));
13.17
14.1 --- a/src/Pure/PIDE/document.ML Mon Jul 11 18:44:58 2011 +0200
14.2 +++ b/src/Pure/PIDE/document.ML Mon Jul 11 23:20:40 2011 +0200
14.3 @@ -252,8 +252,8 @@
14.4 val path = Path.explode thy_name;
14.5 val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
14.6 in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
14.7 - | NONE => Exn.Result raw_tr) of
14.8 - Exn.Result tr =>
14.9 + | NONE => Exn.Res raw_tr) of
14.10 + Exn.Res tr =>
14.11 let
14.12 val is_init = is_some (Toplevel.init_of tr);
14.13 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
15.1 --- a/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 18:44:58 2011 +0200
15.2 +++ b/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 23:20:40 2011 +0200
15.3 @@ -197,7 +197,7 @@
15.4 (* decode_term -- transform parse tree into raw term *)
15.5
15.6 fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
15.7 - | decode_term ctxt (reports0, Exn.Result tm) =
15.8 + | decode_term ctxt (reports0, Exn.Res tm) =
15.9 let
15.10 fun get_const a =
15.11 ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
15.12 @@ -259,7 +259,7 @@
15.13
15.14 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
15.15
15.16 -fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
15.17 +fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
15.18 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
15.19
15.20 fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
15.21 @@ -361,7 +361,7 @@
15.22 else [];
15.23
15.24 (*brute-force disambiguation via type-inference*)
15.25 - fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
15.26 + fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
15.27 handle exn as ERROR _ => Exn.Exn exn;
15.28
15.29 val results' =
16.1 --- a/src/Pure/System/invoke_scala.ML Mon Jul 11 18:44:58 2011 +0200
16.2 +++ b/src/Pure/System/invoke_scala.ML Mon Jul 11 23:20:40 2011 +0200
16.3 @@ -48,7 +48,7 @@
16.4 val result =
16.5 (case tag of
16.6 "0" => Exn.Exn Null
16.7 - | "1" => Exn.Result res
16.8 + | "1" => Exn.Res res
16.9 | "2" => Exn.Exn (ERROR res)
16.10 | "3" => Exn.Exn (Fail res)
16.11 | _ => raise Fail "Bad tag");
17.1 --- a/src/Pure/library.scala Mon Jul 11 18:44:58 2011 +0200
17.2 +++ b/src/Pure/library.scala Mon Jul 11 23:20:40 2011 +0200
17.3 @@ -20,14 +20,19 @@
17.4 {
17.5 /* user errors */
17.6
17.7 + private val runtime_exception = Class.forName("java.lang.RuntimeException")
17.8 +
17.9 object ERROR
17.10 {
17.11 def apply(message: String): Throwable = new RuntimeException(message)
17.12 def unapply(exn: Throwable): Option[String] =
17.13 exn match {
17.14 case e: RuntimeException =>
17.15 - val msg = e.getMessage
17.16 - Some(if (msg == null) "Error" else msg)
17.17 + if (e.getClass != runtime_exception) Some(e.toString)
17.18 + else {
17.19 + val msg = e.getMessage
17.20 + Some(if (msg == null) "Error" else msg)
17.21 + }
17.22 case _ => None
17.23 }
17.24 }
18.1 --- a/src/Pure/proofterm.ML Mon Jul 11 18:44:58 2011 +0200
18.2 +++ b/src/Pure/proofterm.ML Mon Jul 11 23:20:40 2011 +0200
18.3 @@ -217,7 +217,7 @@
18.4 else
18.5 let val seen' = Inttab.update (i, ()) seen in
18.6 (case Future.peek body of
18.7 - SOME (Exn.Result body') => status body' (st, seen')
18.8 + SOME (Exn.Res body') => status body' (st, seen')
18.9 | SOME (Exn.Exn _) =>
18.10 let val (oracle, unfinished, _) = st
18.11 in ((oracle, unfinished, true), seen') end
19.1 --- a/src/Pure/thm.ML Mon Jul 11 18:44:58 2011 +0200
19.2 +++ b/src/Pure/thm.ML Mon Jul 11 23:20:40 2011 +0200
19.3 @@ -528,7 +528,7 @@
19.4 let
19.5 val ps = map (Future.peek o snd) promises;
19.6 val bodies = body ::
19.7 - map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
19.8 + map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
19.9 val {oracle, unfinished, failed} = Proofterm.status_of bodies;
19.10 in
19.11 {oracle = oracle,
20.1 --- a/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 18:44:58 2011 +0200
20.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 23:20:40 2011 +0200
20.3 @@ -214,37 +214,33 @@
20.4 r2 <- r1.try_restrict(chunk_range)
20.5 } yield r2
20.6
20.7 + val padded_markup =
20.8 + if (markup.isEmpty)
20.9 + Iterator(Text.Info(chunk_range, None))
20.10 + else
20.11 + Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
20.12 + markup.iterator ++
20.13 + Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
20.14 +
20.15 var x1 = x + w
20.16 gfx.setFont(chunk_font)
20.17 - if (markup.isEmpty) {
20.18 - gfx.setColor(chunk_color)
20.19 - gfx.drawString(chunk.str, x1, y)
20.20 - }
20.21 - else {
20.22 - for {
20.23 - Text.Info(range, info) <-
20.24 - Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
20.25 - markup.iterator ++
20.26 - Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
20.27 - if !range.is_singularity
20.28 - } {
20.29 - val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
20.30 - gfx.setColor(info.getOrElse(chunk_color))
20.31 + for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
20.32 + val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
20.33 + gfx.setColor(info.getOrElse(chunk_color))
20.34
20.35 - range.try_restrict(caret_range) match {
20.36 - case Some(r) if !r.is_singularity =>
20.37 - val astr = new AttributedString(str)
20.38 - val i = r.start - range.start
20.39 - val j = r.stop - range.start
20.40 - astr.addAttribute(TextAttribute.FONT, chunk_font)
20.41 - astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
20.42 - astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
20.43 - gfx.drawString(astr.getIterator, x1, y)
20.44 - case _ =>
20.45 - gfx.drawString(str, x1, y)
20.46 - }
20.47 - x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
20.48 + range.try_restrict(caret_range) match {
20.49 + case Some(r) if !r.is_singularity =>
20.50 + val astr = new AttributedString(str)
20.51 + val i = r.start - range.start
20.52 + val j = r.stop - range.start
20.53 + astr.addAttribute(TextAttribute.FONT, chunk_font)
20.54 + astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
20.55 + astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
20.56 + gfx.drawString(astr.getIterator, x1, y)
20.57 + case _ =>
20.58 + gfx.drawString(str, x1, y)
20.59 }
20.60 + x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
20.61 }
20.62 }
20.63 w += chunk.width
21.1 --- a/src/Tools/quickcheck.ML Mon Jul 11 18:44:58 2011 +0200
21.2 +++ b/src/Tools/quickcheck.ML Mon Jul 11 23:20:40 2011 +0200
21.3 @@ -237,9 +237,9 @@
21.4 if Config.get ctxt quiet then
21.5 try tester v
21.6 else
21.7 - let
21.8 + let (* FIXME !?!? *)
21.9 val tester = Exn.interruptible_capture tester v
21.10 - in case Exn.get_result tester of
21.11 + in case Exn.get_res tester of
21.12 NONE => SOME (Exn.release tester)
21.13 | SOME tester => SOME tester
21.14 end