1.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Sat Feb 26 12:53:00 2011 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -1,25 +1,36 @@
     1.4 -(*
     1.5 +(* Title:   test/Tools/isac/ADDTESTS/file-depend
     1.6 +   Author:  Walther Neuper
     1.7 +*)
     1.8 +
     1.9 +header {* Test file dependencies analogous to ISAC
    1.10 +
    1.11  $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend
    1.12  $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy &
    1.13 -
    1.14 -*)
    1.15 -
    1.16 +*}
    1.17 +(*----------------------------------------------------------------------------
    1.18  theory Build_Test 
    1.19  imports 
    1.20    Complex_Main 
    1.21    "1language/Foo_Language"
    1.22    "3knowledge/Foo_KnowALL"
    1.23  begin
    1.24 +----------------------------------------------------------------------------*)
    1.25  
    1.26 -use     "0foolibrary.ML"
    1.27 -use_thy "1language/Foo_Language"
    1.28 -use     "2interpreter/2foointerpreter.ML"
    1.29 +theory Build_Test 
    1.30 +imports 
    1.31 +  Complex_Main 
    1.32 +begin
    1.33 +  use     "0foolibrary.ML"                    ML {* foolibrhs *}
    1.34 +  use_thy "1language/Foo_Language"          (*ML {* @{const fooprog} *}*)
    1.35 +  use     "2interpreter/2foointerpreter.ML"   ML {* foointerpret *}
    1.36  
    1.37 -(*vvvvvvv can be bypassed with Foo_KnowALL
    1.38 -use_thy "3knowledge/Foo_Know111"
    1.39 -use_thy "3knowledge/Foo_Know222"
    1.40 -  ^^^^^^^ can be bypassed with Foo_KnowALL*)
    1.41 -use_thy "3knowledge/Foo_KnowALL"
    1.42 +text {* The top 'theory ... begin' can be outcommended and done stepwise:
    1.43 +
    1.44 +  use     "2interpreter/2foointerpreter.ML"
    1.45 +  use_thy "3knowledge/Foo_Know111"
    1.46 +  use_thy "3knowledge/Foo_Know222"
    1.47 +  use_thy "3knowledge/Foo_KnowALL"
    1.48 +*}
    1.49  
    1.50  text {* the different theories of knowledge are recognized, Const bar*: *}
    1.51  ML {* 
    1.52 @@ -48,4 +59,18 @@
    1.53       (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $
    1.54         Free ("bar111", "'a"))
    1.55     : term*)
    1.56 +*}
    1.57 +
    1.58 +text {* dir structure reflects ISAC, see Build_Isac.thy:
    1.59 +/file-depend/0foolibrary.ML
    1.60 +/file-depend/Build_Test.thy
    1.61 +/file-depend/README
    1.62 +
    1.63 +/file-depend/1language/Foo_Language.thy
    1.64 +
    1.65 +/file-depend/2interpreter/2foointerpreter.ML
    1.66 +
    1.67 +/file-depend/3knowledge/Foo_Know111.thy
    1.68 +/file-depend/3knowledge/Foo_Know222.thy
    1.69 +/file-depend/3knowledge/Foo_KnowALL.thy
    1.70  *}
    1.71 \ No newline at end of file