src/Pure/Thy/thy_info.ML
changeset 6900 29060d9b60d4
parent 6666 be06ed5d0b4c
child 7066 febce8eee487
equal deleted inserted replaced
6899:020314dadebd 6900:29060d9b60d4
   291 
   291 
   292 (* begin / end theory *)                (* FIXME tune *) (* FIXME files vs. paths (!?!?) *)
   292 (* begin / end theory *)                (* FIXME tune *) (* FIXME files vs. paths (!?!?) *)
   293 
   293 
   294 fun begin_theory name parents paths =
   294 fun begin_theory name parents paths =
   295   let
   295   let
       
   296     val _ =
       
   297       if is_some (lookup_thy name) andalso is_finished name then
       
   298         error (loader_msg "cannot change finished theory" [name])
       
   299       else ();
   296     val _ = (map Path.basic parents; seq weak_use_thy parents);
   300     val _ = (map Path.basic parents; seq weak_use_thy parents);
   297     val theory = PureThy.begin_theory name (map get_theory parents);
   301     val theory = PureThy.begin_theory name (map get_theory parents);
   298     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
   302     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
   299     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   303     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   300   in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
   304   in Context.setmp (Some theory) (seq use_path) use_paths; theory end;