Toplevel.excursion_error;
authorwenzelm
Thu Jul 22 20:53:26 1999 +0200 (1999-07-22)
changeset 7062e992884b256d
parent 7061 69d42b56151f
child 7063 06ae685ca5a3
Toplevel.excursion_error;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 20:52:58 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 20:53:26 1999 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4      val tr_name = if time then "time_use" else "use";
     1.5    in
     1.6      if not ml orelse is_none (ThyLoad.check_file path) then ()
     1.7 -    else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
     1.8 +    else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
     1.9    end;
    1.10  
    1.11  fun parse_thy (src, pos) =
    1.12 @@ -323,8 +323,7 @@
    1.13    let val (src, pos) = File.source path in
    1.14      Present.theory_source name src;
    1.15      if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
    1.16 -    else (Toplevel.excursion (parse_thy (src, pos))
    1.17 -      handle exn => error (Toplevel.exn_message exn))
    1.18 +    else Toplevel.excursion_error (parse_thy (src, pos))
    1.19    end;
    1.20  
    1.21  fun load_thy name ml time path =
     2.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:52:58 1999 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:53:26 1999 +0200
     2.3 @@ -49,6 +49,7 @@
     2.4    val exn_message: exn -> string
     2.5    val apply: bool -> transition -> state -> (state * (exn * string) option) option
     2.6    val excursion: transition list -> unit
     2.7 +  val excursion_error: transition list -> unit
     2.8    val set_state: state -> unit
     2.9    val get_state: unit -> state
    2.10    val exn: unit -> (exn * string) option
    2.11 @@ -403,6 +404,9 @@
    2.12      State [] => ()
    2.13    | _ => raise ERROR_MESSAGE "Open block(s) pending at end of input");
    2.14  
    2.15 +fun excursion_error trs =
    2.16 +  excursion trs handle exn => error (exn_message exn);
    2.17 +
    2.18  end;
    2.19  
    2.20