Added check that Theory.ML does not occur in the files section of the theory
authorskalberg
Wed Mar 31 16:10:53 2004 +0200 (2004-03-31)
changeset 14503255ad604e08e
parent 14502 0c135fa75626
child 14504 7a3d80e276d4
Added check that Theory.ML does not occur in the files section of the theory
Theory.
NEWS
src/Pure/Isar/isar_thy.ML
     1.1 --- a/NEWS	Wed Mar 31 11:02:00 2004 +0200
     1.2 +++ b/NEWS	Wed Mar 31 16:10:53 2004 +0200
     1.3 @@ -45,6 +45,11 @@
     1.4    later.  It is useful for constants whose behaviour is fixed axiomatically
     1.5    rather than definitionally, such as the meta-logic connectives.
     1.6  
     1.7 +* Pure: It is now illegal to specify Theory.ML explicitly as a dependency
     1.8 +  in the files section of the theory Theory. (This is more of a diagnostic
     1.9 +  than a restriction, as the theory loader screws up if Theory.ML is manually
    1.10 +  loaded.)
    1.11 +
    1.12  *** Isar ***
    1.13  
    1.14  * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Mar 31 11:02:00 2004 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 31 16:10:53 2004 +0200
     2.3 @@ -577,7 +577,11 @@
     2.4  (* theory init and exit *)
     2.5  
     2.6  fun gen_begin_theory upd name parents files =
     2.7 -  ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files);
     2.8 +  let val ml_filename = Path.pack (ThyLoad.ml_path name);
     2.9 +      val () = if exists (equal ml_filename o #1) files
    2.10 +               then error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name)
    2.11 +               else ()
    2.12 +  in ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files) end;
    2.13  
    2.14  val begin_theory = gen_begin_theory false;
    2.15