more basic file dependencies -- no load command here;
authorwenzelm
Thu Aug 23 12:55:23 2012 +0200 (2012-08-23)
changeset 489015e0455e29339
parent 48900 e54cf66928e6
child 48902 44a6967240b7
more basic file dependencies -- no load command here;
src/HOL/Quickcheck_Narrowing.thy
src/HOL/ROOT
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Aug 23 12:44:52 2012 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Aug 23 12:55:23 2012 +0200
     1.3 @@ -5,9 +5,6 @@
     1.4  theory Quickcheck_Narrowing
     1.5  imports Quickcheck_Exhaustive
     1.6  keywords "find_unused_assms" :: diag
     1.7 -uses  (* FIXME session files *)
     1.8 -  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     1.9 -  ("Tools/Quickcheck/Narrowing_Engine.hs")
    1.10  begin
    1.11  
    1.12  subsection {* Counterexample generator *}
     2.1 --- a/src/HOL/ROOT	Thu Aug 23 12:44:52 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Thu Aug 23 12:55:23 2012 +0200
     2.3 @@ -2,7 +2,11 @@
     2.4    description {* Classical Higher-order Logic *}
     2.5    options [document_graph]
     2.6    theories Complex_Main
     2.7 -  files "document/root.bib" "document/root.tex"
     2.8 +  files
     2.9 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    2.10 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    2.11 +    "document/root.bib"
    2.12 +    "document/root.tex"
    2.13  
    2.14  session "HOL-Base" = Pure +
    2.15    description {* Raw HOL base, with minimal tools *}
    2.16 @@ -18,11 +22,17 @@
    2.17    description {* HOL side-entry for Main only, without Complex_Main *}
    2.18    options [document = false]
    2.19    theories Main
    2.20 +  files
    2.21 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    2.22 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    2.23  
    2.24  session "HOL-Proofs" = Pure +
    2.25    description {* HOL-Main with explicit proof terms *}
    2.26    options [document = false, proofs = 2, parallel_proofs = 0]
    2.27    theories Main
    2.28 +  files
    2.29 +    "Tools/Quickcheck/Narrowing_Engine.hs"
    2.30 +    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    2.31  
    2.32  session "HOL-Library" in Library = HOL +
    2.33    description {* Classical Higher-order Logic -- batteries included *}
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 23 12:44:52 2012 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Aug 23 12:55:23 2012 +0200
     3.3 @@ -202,12 +202,10 @@
     3.4  (** invocation of Haskell interpreter **)
     3.5  
     3.6  val narrowing_engine =
     3.7 -  Context.>>> (Context.map_theory_result
     3.8 -    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/Narrowing_Engine.hs")))
     3.9 +  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
    3.10  
    3.11  val pnf_narrowing_engine =
    3.12 -  Context.>>> (Context.map_theory_result
    3.13 -    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/PNF_Narrowing_Engine.hs")))
    3.14 +  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    3.15  
    3.16  fun exec verbose code =
    3.17    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)