src/Pure/Thy/thy_read.ML
changeset 5615 9ea709aa275c
parent 5495 48036910ab7e
child 5730 82a7aa74a631
equal deleted inserted replaced
5614:0e8b45a7d104 5615:9ea709aa275c
   247 	   if thy_file = "" then ()
   247 	   if thy_file = "" then ()
   248 	   else
   248 	   else
   249 	     (writeln ("Reading \"" ^ name ^ ".thy\"");
   249 	     (writeln ("Reading \"" ^ name ^ ".thy\"");
   250 	      init_thyinfo ();
   250 	      init_thyinfo ();
   251 	      read_thy tname thy_file;
   251 	      read_thy tname thy_file;
   252               let val old_pt = ! Goals.proof_timing;
   252 	      Use.use (out_name tname);
   253 	      in  (*suppress annoying messages during theory loading*)
       
   254 		  proof_timing := false;
       
   255 		  Use.use (out_name tname);
       
   256                   proof_timing := old_pt
       
   257                   end;
       
   258 	      if not (!delete_tmpfiles) then ()
   253 	      if not (!delete_tmpfiles) then ()
   259 	      else OS.FileSys.remove (out_name tname);
   254 	      else OS.FileSys.remove (out_name tname);
   260 	      thyfile2html tname abs_path)
   255 	      thyfile2html tname abs_path)
   261 
   256 
   262        (*Add theory to list of all loaded theories (for index.html)
   257        (*Add theory to list of all loaded theories (for index.html)
   292 val use_thy = use_thy1 false;
   287 val use_thy = use_thy1 false;
   293 
   288 
   294 
   289 
   295 fun time_use_thy tname = timeit(fn()=>
   290 fun time_use_thy tname = timeit(fn()=>
   296    (writeln("\n**** Starting Theory " ^ tname ^ " ****");
   291    (writeln("\n**** Starting Theory " ^ tname ^ " ****");
   297     use_thy tname;
   292     setmp Goals.proof_timing true use_thy tname;
   298     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   293     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   299    );
   294    );
   300 
   295 
   301 
   296 
   302 (*Load all thy or ML files that have been changed and also
   297 (*Load all thy or ML files that have been changed and also