src/Pure/ROOT.ML
changeset 60956 10d463883dc2
parent 60937 51425cbe8ce9
child 60957 574254152856
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 15:29:30 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
     1.3 @@ -41,10 +41,10 @@
     1.4  val use_text = Secure.use_text;
     1.5  val use_file = Secure.use_file;
     1.6  
     1.7 -fun use s =
     1.8 -  Position.setmp_thread_data (Position.file_only s)
     1.9 +fun use file =
    1.10 +  Position.setmp_thread_data (Position.file_only file)
    1.11      (fn () =>
    1.12 -      Secure.use_file ML_Parse.global_context true s
    1.13 +      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    1.14          handle ERROR msg => (writeln msg; error "ML error")) ();
    1.15  
    1.16  val toplevel_pp = Secure.toplevel_pp;