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;
authorwenzelm
Tue Jul 20 14:44:33 2010 +0200 (2010-07-20 ago)
changeset 37852a902f158b4fc
parent 37851 1ce77362598f
child 37853 26906cacbaae
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;
src/Pure/Concurrent/future.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/context.ML
src/Pure/term_ord.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 20 14:41:13 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 20 14:44:33 2010 +0200
     1.3 @@ -409,7 +409,7 @@
     1.4  
     1.5  fun get_result x =
     1.6    (case peek x of
     1.7 -    NONE => Exn.Exn (SYS_ERROR "unfinished future")
     1.8 +    NONE => Exn.Exn (Fail "Unfinished future")
     1.9    | SOME (exn as Exn.Exn Exn.Interrupt) =>
    1.10        (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    1.11          [] => exn
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 20 14:41:13 2010 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 20 14:44:33 2010 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4    (case cmd name of
     2.5      SOME (Command {int_only, parse, ...}) =>
     2.6        Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
     2.7 -  | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
     2.8 +  | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
     2.9  
    2.10  in
    2.11  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 14:41:13 2010 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 14:44:33 2010 +0200
     3.3 @@ -699,7 +699,7 @@
     3.4  
     3.5          val states =
     3.6            (case States.get (presentation_context_of st'') of
     3.7 -            NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
     3.8 +            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
     3.9            | SOME states => states);
    3.10          val result = Lazy.lazy
    3.11            (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
     4.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 20 14:41:13 2010 +0200
     4.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 20 14:44:33 2010 +0200
     4.3 @@ -78,7 +78,7 @@
     4.4    |> command Keyword.prf_script       proofstep;
     4.5  
     4.6  val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
     4.7 -  orelse sys_error "Incomplete coverage of command keywords";
     4.8 +  orelse raise Fail "Incomplete coverage of command keywords";
     4.9  
    4.10  fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    4.11    | parse_command name text =
     5.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 20 14:41:13 2010 +0200
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 20 14:44:33 2010 +0200
     5.3 @@ -505,7 +505,7 @@
     5.4          isarcmd ("undos_proof " ^ Int.toString times)
     5.5      end
     5.6  
     5.7 -fun redostep _ = sys_error "redo unavailable"
     5.8 +fun redostep _ = raise Fail "redo unavailable"
     5.9  
    5.10  fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
    5.11  
     6.1 --- a/src/Pure/Syntax/parser.ML	Tue Jul 20 14:41:13 2010 +0200
     6.2 +++ b/src/Pure/Syntax/parser.ML	Tue Jul 20 14:44:33 2010 +0200
     6.3 @@ -828,7 +828,7 @@
     6.4        | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     6.5      val r =
     6.6        (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
     6.7 -        [] => raise Fail "no parse trees"
     6.8 +        [] => raise Fail "Inner syntax: no parse trees"
     6.9        | pts => pts);
    6.10    in r end;
    6.11  
     7.1 --- a/src/Pure/Syntax/printer.ML	Tue Jul 20 14:41:13 2010 +0200
     7.2 +++ b/src/Pure/Syntax/printer.ML	Tue Jul 20 14:44:33 2010 +0200
     7.3 @@ -80,7 +80,7 @@
     7.4          Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
     7.5        end
     7.6    | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
     7.7 -  | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
     7.8 +  | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
     7.9  
    7.10  
    7.11  
    7.12 @@ -246,7 +246,7 @@
    7.13        in
    7.14          (case xsyms_to_syms xsymbs of
    7.15            (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
    7.16 -        | _ => sys_error "xprod_to_fmt: unbalanced blocks")
    7.17 +        | _ => raise Fail "Unbalanced pretty-printing blocks")
    7.18        end;
    7.19  
    7.20  
     8.1 --- a/src/Pure/context.ML	Tue Jul 20 14:41:13 2010 +0200
     8.2 +++ b/src/Pure/context.ML	Tue Jul 20 14:44:33 2010 +0200
     8.3 @@ -120,7 +120,7 @@
     8.4  fun invoke f k =
     8.5    (case Datatab.lookup (! kinds) k of
     8.6      SOME kind => f kind
     8.7 -  | NONE => sys_error "Invalid theory data identifier");
     8.8 +  | NONE => raise Fail "Invalid theory data identifier");
     8.9  
    8.10  in
    8.11  
    8.12 @@ -459,7 +459,7 @@
    8.13  fun invoke_init k =
    8.14    (case Datatab.lookup (! kinds) k of
    8.15      SOME init => init
    8.16 -  | NONE => sys_error "Invalid proof data identifier");
    8.17 +  | NONE => raise Fail "Invalid proof data identifier");
    8.18  
    8.19  fun init_data thy =
    8.20    Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
     9.1 --- a/src/Pure/term_ord.ML	Tue Jul 20 14:41:13 2010 +0200
     9.2 +++ b/src/Pure/term_ord.ML	Tue Jul 20 14:44:33 2010 +0200
     9.3 @@ -84,7 +84,7 @@
     9.4    | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
     9.5    | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
     9.6    | atoms_ord (Bound i, Bound j) = int_ord (i, j)
     9.7 -  | atoms_ord _ = sys_error "atoms_ord";
     9.8 +  | atoms_ord _ = raise Fail "atoms_ord";
     9.9  
    9.10  fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
    9.11        (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
    9.12 @@ -94,7 +94,7 @@
    9.13    | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
    9.14    | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
    9.15    | types_ord (Bound _, Bound _) = EQUAL
    9.16 -  | types_ord _ = sys_error "types_ord";
    9.17 +  | types_ord _ = raise Fail "types_ord";
    9.18  
    9.19  in
    9.20