tuned error, according to "use" in General/secure.ML;
authorwenzelm
Thu Mar 20 19:24:51 2014 +0100 (2014-03-20)
changeset 56229f61eaab6bec3
parent 56228 0f6dc7512023
child 56230 3e449273942a
tuned error, according to "use" in General/secure.ML;
src/Pure/ML/ml_context.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 20 15:38:49 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 19:24:51 2014 +0100
     1.3 @@ -191,3 +191,7 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +fun use s =
     1.8 +  ML_Context.eval_file true (Path.explode s)
     1.9 +    handle ERROR msg => (writeln msg; error "ML error");
    1.10 +
     2.1 --- a/src/Pure/ROOT.ML	Thu Mar 20 15:38:49 2014 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Thu Mar 20 19:24:51 2014 +0100
     2.3 @@ -226,7 +226,6 @@
     2.4  (*ML with context and antiquotations*)
     2.5  use "ML/ml_context.ML";
     2.6  use "ML/ml_antiquotation.ML";
     2.7 -val use = ML_Context.eval_file true o Path.explode;
     2.8  (*^^^^^ end of ML bootstrap 1 ^^^^^*)
     2.9  
    2.10  (*basic proof engine*)