src/Pure/Thy/thy_read.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5209 a69fe5a61b6c
equal deleted inserted replaced
5089:f95e0a6eb775 5090:75ac9b451ae0
   265        if ml_file = "" then ()
   265        if ml_file = "" then ()
   266        else (writeln ("Reading \"" ^ name ^ ".ML\"");
   266        else (writeln ("Reading \"" ^ name ^ ".ML\"");
   267              Use.use ml_file);
   267              Use.use ml_file);
   268 
   268 
   269        (*Store theory again because it could have been redefined*)
   269        (*Store theory again because it could have been redefined*)
   270        use_text ("val _ = store_theory " ^ tname ^ ".thy;");
   270        use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
   271 
   271 
   272        (*Add theory to list of all loaded theories (for index.html)
   272        (*Add theory to list of all loaded theories (for index.html)
   273          and add it to its parents' sub-charts*)
   273          and add it to its parents' sub-charts*)
   274        let val path = path_of tname;
   274        let val path = path_of tname;
   275        in if path = "" then               (*first time theory has been read*)
   275        in if path = "" then               (*first time theory has been read*)