--- a/src/Pure/Concurrent/future.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 11 23:20:40 2011 +0200
@@ -117,7 +117,7 @@
val ok =
(case the (Single_Assignment.peek result) of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
- | Exn.Result _ => true);
+ | Exn.Res _ => true);
in ok end;
@@ -482,7 +482,7 @@
val task = Task_Queue.dummy_task ();
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result (Exn.Result x);
+ val _ = assign_result group result (Exn.Res x);
in Future {promised = false, task = task, result = result} end;
fun map_future f x =
@@ -544,7 +544,7 @@
else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
in () end;
-fun fulfill x res = fulfill_result x (Exn.Result res);
+fun fulfill x res = fulfill_result x (Exn.Res res);
(* cancellation *)
--- a/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 23:20:40 2011 +0200
@@ -23,7 +23,7 @@
| Result res => SOME res);
fun lazy e = Lazy (Unsynchronized.ref (Expr e));
-fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
(* force result *)
--- a/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 23:20:40 2011 +0200
@@ -38,7 +38,7 @@
(case peek v of
NONE =>
(case Multithreading.sync_wait NONE NONE cond lock of
- Exn.Result _ => wait ()
+ Exn.Res _ => wait ()
| Exn.Exn exn => reraise exn)
| SOME x => x);
in wait () end);
--- a/src/Pure/Concurrent/synchronized.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Mon Jul 11 23:20:40 2011 +0200
@@ -47,8 +47,8 @@
(case f x of
NONE =>
(case Multithreading.sync_wait NONE (time_limit x) cond lock of
- Exn.Result true => try_change ()
- | Exn.Result false => NONE
+ Exn.Res true => try_change ()
+ | Exn.Res false => NONE
| Exn.Exn exn => reraise exn)
| SOME (y, x') =>
uninterruptible (fn _ => fn () =>
--- a/src/Pure/General/exn.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/exn.ML Mon Jul 11 23:20:40 2011 +0200
@@ -1,13 +1,13 @@
(* Title: Pure/General/exn.ML
Author: Makarius
-Extra support for exceptions.
+Support for exceptions.
*)
signature EXN =
sig
- datatype 'a result = Result of 'a | Exn of exn
- val get_result: 'a result -> 'a option
+ datatype 'a result = Res of 'a | Exn of exn
+ val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
@@ -33,24 +33,24 @@
(* runtime exceptions as values *)
datatype 'a result =
- Result of 'a |
+ Res of 'a |
Exn of exn;
-fun get_result (Result x) = SOME x
- | get_result _ = NONE;
+fun get_res (Res x) = SOME x
+ | get_res _ = NONE;
fun get_exn (Exn exn) = SOME exn
| get_exn _ = NONE;
-fun capture f x = Result (f x) handle e => Exn e;
+fun capture f x = Res (f x) handle e => Exn e;
-fun release (Result y) = y
+fun release (Res y) = y
| release (Exn e) = reraise e;
-fun flat_result (Result x) = x
+fun flat_result (Res x) = x
| flat_result (Exn e) = Exn e;
-fun map_result f (Result x) = Result (f x)
+fun map_result f (Res x) = Res (f x)
| map_result f (Exn e) = Exn e;
fun maps_result f = flat_result o map_result f;
@@ -72,7 +72,7 @@
| is_interrupt_exn _ = false;
fun interruptible_capture f x =
- Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
+ Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
(* nested exceptions *)
@@ -84,8 +84,8 @@
and flatten_list exns = List.concat (map flatten exns);
fun release_all results =
- if List.all (fn Result _ => true | _ => false) results
- then map (fn Result x => x) results
+ if List.all (fn Res _ => true | _ => false) results
+ then map (fn Res x => x) results
else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
fun release_first results = release_all results
--- a/src/Pure/General/exn.scala Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/exn.scala Mon Jul 11 23:20:40 2011 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/General/exn.scala
Author: Makarius
-Extra support for exceptions (arbitrary throwables).
+Support for exceptions (arbitrary throwables).
*/
package isabelle
@@ -12,8 +12,8 @@
/* runtime exceptions as values */
sealed abstract class Result[A]
- case class Res[A](val result: A) extends Result[A]
- case class Exn[A](val exn: Throwable) extends Result[A]
+ case class Res[A](res: A) extends Result[A]
+ case class Exn[A](exn: Throwable) extends Result[A]
def capture[A](e: => A): Result[A] =
try { Res(e) }
--- a/src/Pure/General/output.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/General/output.ML Mon Jul 11 23:20:40 2011 +0200
@@ -96,9 +96,8 @@
val prompt_fn = Unsynchronized.ref raw_stdout;
val status_fn = Unsynchronized.ref (fn _: output => ());
val report_fn = Unsynchronized.ref (fn _: output => ());
- val raw_message_fn =
- Unsynchronized.ref
- (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
+ val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+ Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
end;
fun writeln s = ! Private_Hooks.writeln_fn (output s);
--- a/src/Pure/Isar/proof.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 11 23:20:40 2011 +0200
@@ -1008,8 +1008,8 @@
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
|> int ? (fn goal_state =>
(case test_proof goal_state of
- Exn.Result (SOME _) => goal_state
- | Exn.Result NONE => error (fail_msg (context_of goal_state))
+ Exn.Res (SOME _) => goal_state
+ | Exn.Res NONE => error (fail_msg (context_of goal_state))
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
--- a/src/Pure/Isar/runtime.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Isar/runtime.ML Mon Jul 11 23:20:40 2011 +0200
@@ -101,7 +101,7 @@
fun debugging f x =
if ! debug then
Exn.release (exception_trace (fn () =>
- Exn.Result (f x) handle
+ Exn.Res (f x) handle
exn as UNDEF => Exn.Exn exn
| exn as EXCURSION_FAIL _ => Exn.Exn exn))
else f x;
--- a/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 23:20:40 2011 +0200
@@ -55,7 +55,7 @@
fun with_attributes _ e = e [];
-fun sync_wait _ _ _ _ = Exn.Result true;
+fun sync_wait _ _ _ _ = Exn.Res true;
(* tracing *)
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 23:20:40 2011 +0200
@@ -97,8 +97,8 @@
(sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
(fn _ =>
(case time of
- SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
- | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
+ SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
+ | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
handle exn => Exn.Exn exn);
--- a/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 23:20:40 2011 +0200
@@ -14,13 +14,13 @@
(case Future.peek x of
NONE => PolyML.PrettyString "<future>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
+ | SOME (Exn.Res y) => pretty (y, depth)));
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
(case Lazy.peek x of
NONE => PolyML.PrettyString "<lazy>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
+ | SOME (Exn.Res y) => pretty (y, depth)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
let
--- a/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 23:20:40 2011 +0200
@@ -9,12 +9,12 @@
(case Future.peek x of
NONE => str "<future>"
| SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+ | SOME (Exn.Res y) => print (y, depth)));
PolyML.install_pp
(fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
(case Lazy.peek x of
NONE => str "<lazy>"
| SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+ | SOME (Exn.Res y) => print (y, depth)));
--- a/src/Pure/PIDE/document.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/PIDE/document.ML Mon Jul 11 23:20:40 2011 +0200
@@ -252,8 +252,8 @@
val path = Path.explode thy_name;
val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
- | NONE => Exn.Result raw_tr) of
- Exn.Result tr =>
+ | NONE => Exn.Res raw_tr) of
+ Exn.Res tr =>
let
val is_init = is_some (Toplevel.init_of tr);
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
--- a/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 23:20:40 2011 +0200
@@ -197,7 +197,7 @@
(* decode_term -- transform parse tree into raw term *)
fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
- | decode_term ctxt (reports0, Exn.Result tm) =
+ | decode_term ctxt (reports0, Exn.Res tm) =
let
fun get_const a =
((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
@@ -259,7 +259,7 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun proper_results results = map_filter (fn (y, Exn.Res 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);
@@ -361,7 +361,7 @@
else [];
(*brute-force disambiguation via type-inference*)
- fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
+ fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
handle exn as ERROR _ => Exn.Exn exn;
val results' =
--- a/src/Pure/System/invoke_scala.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML Mon Jul 11 23:20:40 2011 +0200
@@ -48,7 +48,7 @@
val result =
(case tag of
"0" => Exn.Exn Null
- | "1" => Exn.Result res
+ | "1" => Exn.Res res
| "2" => Exn.Exn (ERROR res)
| "3" => Exn.Exn (Fail res)
| _ => raise Fail "Bad tag");
--- a/src/Pure/library.scala Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/library.scala Mon Jul 11 23:20:40 2011 +0200
@@ -20,14 +20,19 @@
{
/* user errors */
+ private val runtime_exception = Class.forName("java.lang.RuntimeException")
+
object ERROR
{
def apply(message: String): Throwable = new RuntimeException(message)
def unapply(exn: Throwable): Option[String] =
exn match {
case e: RuntimeException =>
- val msg = e.getMessage
- Some(if (msg == null) "Error" else msg)
+ if (e.getClass != runtime_exception) Some(e.toString)
+ else {
+ val msg = e.getMessage
+ Some(if (msg == null) "Error" else msg)
+ }
case _ => None
}
}
--- a/src/Pure/proofterm.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/proofterm.ML Mon Jul 11 23:20:40 2011 +0200
@@ -217,7 +217,7 @@
else
let val seen' = Inttab.update (i, ()) seen in
(case Future.peek body of
- SOME (Exn.Result body') => status body' (st, seen')
+ SOME (Exn.Res body') => status body' (st, seen')
| SOME (Exn.Exn _) =>
let val (oracle, unfinished, _) = st
in ((oracle, unfinished, true), seen') end
--- a/src/Pure/thm.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Pure/thm.ML Mon Jul 11 23:20:40 2011 +0200
@@ -528,7 +528,7 @@
let
val ps = map (Future.peek o snd) promises;
val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
val {oracle, unfinished, failed} = Proofterm.status_of bodies;
in
{oracle = oracle,
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 23:20:40 2011 +0200
@@ -214,37 +214,33 @@
r2 <- r1.try_restrict(chunk_range)
} yield r2
+ val padded_markup =
+ if (markup.isEmpty)
+ Iterator(Text.Info(chunk_range, None))
+ else
+ Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
+ markup.iterator ++
+ Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
+
var x1 = x + w
gfx.setFont(chunk_font)
- if (markup.isEmpty) {
- gfx.setColor(chunk_color)
- gfx.drawString(chunk.str, x1, y)
- }
- else {
- for {
- Text.Info(range, info) <-
- Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
- markup.iterator ++
- Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
- if !range.is_singularity
- } {
- val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
- gfx.setColor(info.getOrElse(chunk_color))
+ for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
+ val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+ gfx.setColor(info.getOrElse(chunk_color))
- range.try_restrict(caret_range) match {
- case Some(r) if !r.is_singularity =>
- val astr = new AttributedString(str)
- val i = r.start - range.start
- val j = r.stop - range.start
- astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
- gfx.drawString(astr.getIterator, x1, y)
- case _ =>
- gfx.drawString(str, x1, y)
- }
- x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ range.try_restrict(caret_range) match {
+ case Some(r) if !r.is_singularity =>
+ val astr = new AttributedString(str)
+ val i = r.start - range.start
+ val j = r.stop - range.start
+ astr.addAttribute(TextAttribute.FONT, chunk_font)
+ astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
+ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
+ gfx.drawString(astr.getIterator, x1, y)
+ case _ =>
+ gfx.drawString(str, x1, y)
}
+ x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
}
}
w += chunk.width
--- a/src/Tools/quickcheck.ML Mon Jul 11 18:44:58 2011 +0200
+++ b/src/Tools/quickcheck.ML Mon Jul 11 23:20:40 2011 +0200
@@ -237,9 +237,9 @@
if Config.get ctxt quiet then
try tester v
else
- let
+ let (* FIXME !?!? *)
val tester = Exn.interruptible_capture tester v
- in case Exn.get_result tester of
+ in case Exn.get_res tester of
NONE => SOME (Exn.release tester)
| SOME tester => SOME tester
end