# HG changeset patch
# User wenzelm
# Date 1279629873 -7200
# Node ID a902f158b4fc8c467e7608503940394399af304a
# Parent  1ce77362598f10890a6887bb246e13d38f1f5c6b
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
tuned some error messages;

diff -r 1ce77362598f -r a902f158b4fc src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -409,7 +409,7 @@
 
 fun get_result x =
   (case peek x of
-    NONE => Exn.Exn (SYS_ERROR "unfinished future")
+    NONE => Exn.Exn (Fail "Unfinished future")
   | SOME (exn as Exn.Exn Exn.Interrupt) =>
       (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
         [] => exn
diff -r 1ce77362598f -r a902f158b4fc src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -62,7 +62,7 @@
   (case cmd name of
     SOME (Command {int_only, parse, ...}) =>
       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
-  | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
+  | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
 
 in
 
diff -r 1ce77362598f -r a902f158b4fc src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -699,7 +699,7 @@
 
         val states =
           (case States.get (presentation_context_of st'') of
-            NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
+            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
           | SOME states => states);
         val result = Lazy.lazy
           (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
diff -r 1ce77362598f -r a902f158b4fc src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -78,7 +78,7 @@
   |> command Keyword.prf_script       proofstep;
 
 val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
-  orelse sys_error "Incomplete coverage of command keywords";
+  orelse raise Fail "Incomplete coverage of command keywords";
 
 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
   | parse_command name text =
diff -r 1ce77362598f -r a902f158b4fc src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -505,7 +505,7 @@
         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
-fun redostep _ = sys_error "redo unavailable"
+fun redostep _ = raise Fail "redo unavailable"
 
 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
 
diff -r 1ce77362598f -r a902f158b4fc src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -828,7 +828,7 @@
       | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     val r =
       (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
-        [] => raise Fail "no parse trees"
+        [] => raise Fail "Inner syntax: no parse trees"
       | pts => pts);
   in r end;
 
diff -r 1ce77362598f -r a902f158b4fc src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -80,7 +80,7 @@
         Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
       end
   | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
-  | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
+  | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
 
 
 
@@ -246,7 +246,7 @@
       in
         (case xsyms_to_syms xsymbs of
           (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
-        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
+        | _ => raise Fail "Unbalanced pretty-printing blocks")
       end;
 
 
diff -r 1ce77362598f -r a902f158b4fc src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/context.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -120,7 +120,7 @@
 fun invoke f k =
   (case Datatab.lookup (! kinds) k of
     SOME kind => f kind
-  | NONE => sys_error "Invalid theory data identifier");
+  | NONE => raise Fail "Invalid theory data identifier");
 
 in
 
@@ -459,7 +459,7 @@
 fun invoke_init k =
   (case Datatab.lookup (! kinds) k of
     SOME init => init
-  | NONE => sys_error "Invalid proof data identifier");
+  | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
   Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
diff -r 1ce77362598f -r a902f158b4fc src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/term_ord.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -84,7 +84,7 @@
   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
-  | atoms_ord _ = sys_error "atoms_ord";
+  | atoms_ord _ = raise Fail "atoms_ord";
 
 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
@@ -94,7 +94,7 @@
   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   | types_ord (Bound _, Bound _) = EQUAL
-  | types_ord _ = sys_error "types_ord";
+  | types_ord _ = raise Fail "types_ord";
 
 in