ThyInfo.may_load_file;
authorwenzelm
Tue Aug 17 22:19:48 1999 +0200 (1999-08-17)
changeset 7243886ecd6a27ac
parent 7242 f17f2e8ba0c7
child 7244 ad714526c23e
ThyInfo.may_load_file;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:25 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:48 1999 +0200
     1.3 @@ -286,10 +286,10 @@
     1.4  fun try_ml_file name ml time =
     1.5    let
     1.6      val path = ThyLoad.ml_path name;
     1.7 -    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
     1.8 +    val tr = Toplevel.imperative (fn () => ThyInfo.may_load_file ml time path);
     1.9      val tr_name = if time then "time_use" else "use";
    1.10    in
    1.11 -    if not ml orelse is_none (ThyLoad.check_file path) then ()
    1.12 +    if is_none (ThyLoad.check_file path) then ()
    1.13      else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.14    end;
    1.15