eliminated transform_failure (to avoid critical section for main transactions);
authorwenzelm
Mon Jul 23 19:45:44 2007 +0200 (2007-07-23)
changeset 2393766e1f24d655d
parent 23936 66923825628e
child 23938 977d14aeb4d5
eliminated transform_failure (to avoid critical section for main transactions);
src/Pure/Isar/antiquote.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Isar/antiquote.ML	Mon Jul 23 16:45:04 2007 +0200
     1.2 +++ b/src/Pure/Isar/antiquote.ML	Mon Jul 23 19:45:44 2007 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature ANTIQUOTE =
     1.6  sig
     1.7 -  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
     1.8    datatype antiquote = Text of string | Antiq of string * Position.T
     1.9    val is_antiq: antiquote -> bool
    1.10    val scan_antiquotes: string * Position.T -> antiquote list
    1.11 @@ -20,8 +19,6 @@
    1.12  
    1.13  (* datatype antiquote *)
    1.14  
    1.15 -exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
    1.16 -
    1.17  datatype antiquote =
    1.18    Text of string |
    1.19    Antiq of string * Position.T;
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Jul 23 16:45:04 2007 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Jul 23 19:45:44 2007 +0200
     2.3 @@ -14,7 +14,6 @@
     2.4  sig
     2.5    include BASIC_ATTRIB
     2.6    type src
     2.7 -  exception ATTRIB_FAIL of (string * Position.T) * exn
     2.8    val intern: theory -> xstring -> string
     2.9    val intern_src: theory -> src -> src
    2.10    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    2.11 @@ -87,8 +86,6 @@
    2.12  
    2.13  (* get attributes *)
    2.14  
    2.15 -exception ATTRIB_FAIL of (string * Position.T) * exn;
    2.16 -
    2.17  fun attribute_i thy =
    2.18    let
    2.19      val attrs = #2 (AttributesData.get thy);
    2.20 @@ -96,7 +93,7 @@
    2.21        let val ((name, _), pos) = Args.dest_src src in
    2.22          (case Symtab.lookup attrs name of
    2.23            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    2.24 -        | SOME ((att, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (att src))
    2.25 +        | SOME ((att, _), _) => att src)
    2.26        end;
    2.27    in attr end;
    2.28  
     3.1 --- a/src/Pure/Isar/method.ML	Mon Jul 23 16:45:04 2007 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Mon Jul 23 19:45:44 2007 +0200
     3.3 @@ -69,7 +69,6 @@
     3.4    val done_text: text
     3.5    val sorry_text: bool -> text
     3.6    val finish_text: text option * bool -> Position.T -> text
     3.7 -  exception METHOD_FAIL of (string * Position.T) * exn
     3.8    val method: theory -> src -> Proof.context -> method
     3.9    val method_i: theory -> src -> Proof.context -> method
    3.10    val add_methods: (bstring * (src -> Proof.context -> method) * string) list
    3.11 @@ -406,8 +405,6 @@
    3.12  
    3.13  (* get methods *)
    3.14  
    3.15 -exception METHOD_FAIL of (string * Position.T) * exn;
    3.16 -
    3.17  fun method_i thy =
    3.18    let
    3.19      val meths = #2 (MethodsData.get thy);
    3.20 @@ -415,7 +412,7 @@
    3.21        let val ((name, _), pos) = Args.dest_src src in
    3.22          (case Symtab.lookup meths name of
    3.23            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    3.24 -        | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
    3.25 +        | SOME ((mth, _), _) => mth src)
    3.26        end;
    3.27    in meth end;
    3.28  
     4.1 --- a/src/Pure/Syntax/printer.ML	Mon Jul 23 16:45:04 2007 +0200
     4.2 +++ b/src/Pure/Syntax/printer.ML	Mon Jul 23 19:45:44 2007 +0200
     4.3 @@ -58,15 +58,11 @@
     4.4  
     4.5  (* apply print (ast) translation function *)
     4.6  
     4.7 -fun apply_trans ctxt name a fns args =
     4.8 +fun apply_trans ctxt fns args =
     4.9    let
    4.10      fun app_first [] = raise Match
    4.11        | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
    4.12 -  in
    4.13 -    transform_failure (fn Match => Match
    4.14 -      | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
    4.15 -      app_first fns
    4.16 -  end;
    4.17 +  in app_first fns end;
    4.18  
    4.19  fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
    4.20  
    4.21 @@ -99,7 +95,7 @@
    4.22            | (f, args) => Ast.Appl (map ast_of (f :: args)))
    4.23        | ast_of t = simple_ast_of t
    4.24      and trans a args =
    4.25 -      ast_of (apply_trans ctxt "print translation" a (apply_typed false dummyT (trf a)) args)
    4.26 +      ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
    4.27          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    4.28    in ast_of tm end;
    4.29  
    4.30 @@ -160,7 +156,7 @@
    4.31        | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
    4.32  
    4.33      and trans a T args =
    4.34 -      ast_of (apply_trans ctxt "print translation" a (apply_typed show_sorts T (trf a)) args)
    4.35 +      ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
    4.36          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    4.37  
    4.38      and constrain t T =
    4.39 @@ -270,8 +266,6 @@
    4.40  
    4.41  fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
    4.42    let
    4.43 -    val trans = apply_trans ctxt "print ast translation";
    4.44 -
    4.45      fun token_trans c [Ast.Variable x] =
    4.46            (case tokentrf c of
    4.47              NONE => NONE
    4.48 @@ -359,7 +353,7 @@
    4.49          (case token_trans a args of     (*try token translation function*)
    4.50            SOME s => [Pretty.raw_str s]
    4.51          | NONE =>                       (*try print translation functions*)
    4.52 -            astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
    4.53 +            astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
    4.54        end
    4.55  
    4.56      and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
     5.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Jul 23 16:45:04 2007 +0200
     5.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon Jul 23 19:45:44 2007 +0200
     5.3 @@ -485,9 +485,7 @@
     5.4      fun trans a args =
     5.5        (case trf a of
     5.6          NONE => Ast.mk_appl (Ast.Constant a) args
     5.7 -      | SOME f => transform_failure (fn exn =>
     5.8 -            EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))
     5.9 -          (fn () => f ctxt args) ());
    5.10 +      | SOME f => f ctxt args);
    5.11  
    5.12      (*translate pt bottom-up*)
    5.13      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    5.14 @@ -507,9 +505,7 @@
    5.15      fun trans a args =
    5.16        (case trf a of
    5.17          NONE => Term.list_comb (Lexicon.const a, args)
    5.18 -      | SOME f => transform_failure (fn exn =>
    5.19 -            EXCEPTION (exn, "Error in parse translation for " ^ quote a))
    5.20 -          (fn () => f ctxt args) ());
    5.21 +      | SOME f => f ctxt args);
    5.22  
    5.23      fun term_of (Ast.Constant a) = trans a []
    5.24        | term_of (Ast.Variable x) = Lexicon.read_var x
     6.1 --- a/src/Pure/library.ML	Mon Jul 23 16:45:04 2007 +0200
     6.2 +++ b/src/Pure/library.ML	Mon Jul 23 19:45:44 2007 +0200
     6.3 @@ -34,8 +34,6 @@
     6.4  
     6.5    (*exceptions*)
     6.6    exception EXCEPTION of exn * string
     6.7 -  val do_transform_failure: bool ref
     6.8 -  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
     6.9    datatype 'a result = Result of 'a | Exn of exn
    6.10    val capture: ('a -> 'b) -> 'a -> 'b result
    6.11    val release: 'a result -> 'a
    6.12 @@ -273,13 +271,6 @@
    6.13  
    6.14  (* exceptions *)
    6.15  
    6.16 -val do_transform_failure = ref true;
    6.17 -
    6.18 -fun transform_failure exn f x =
    6.19 -  if ! do_transform_failure then
    6.20 -    f x handle Interrupt => raise Interrupt | e => raise exn e
    6.21 -  else f x;
    6.22 -
    6.23  exception EXCEPTION of exn * string;
    6.24  
    6.25  datatype 'a result =