1.1 --- a/ROOTS	Mon Sep 02 16:16:08 2013 +0200
     1.2 +++ b/ROOTS	Fri Sep 13 18:57:11 2013 +0200
     1.3 @@ -10,4 +10,4 @@
     1.4  src/Sequents
     1.5  src/Doc
     1.6  src/Tools/isac
     1.7 -
     1.8 +test/Tools/isac/ADDTESTS/session-get_theory/

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/test/Tools/isac/ADDTESTS/session-get_theory/Bar.thy	Fri Sep 13 18:57:11 2013 +0200
     2.3 @@ -0,0 +1,5 @@
     2.4 +theory Bar imports Pure begin
     2.5 +ML {*
     2.6 +  val bar_data = "bar_data"
     2.7 +*}
     2.8 +end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/test/Tools/isac/ADDTESTS/session-get_theory/Foo.thy	Fri Sep 13 18:57:11 2013 +0200
     3.3 @@ -0,0 +1,9 @@
     3.4 +theory Foo imports Bar begin
     3.5 +ML {*
     3.6 +  @{theory Bar};           (*OK                                                     *)
     3.7 +(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)
     3.8 +  case Thy_Info.lookup_theory "Bar" of
     3.9 +    NONE => writeln "Expected, if Foo.thy is loaded directly. "
    3.10 +  | SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar."
    3.11 +*}
    3.12 +end

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/test/Tools/isac/ADDTESTS/session-get_theory/ROOT	Fri Sep 13 18:57:11 2013 +0200
     4.3 @@ -0,0 +1,9 @@
     4.4 +session Bar in "~~/test/Tools/isac/ADDTESTS/session-get_theory" = Pure +
     4.5 +  description {*
     4.6 +    Trial to make the theory loader able to 'Thy_Info.get_theory "Bar"' in Foo.thy.
     4.7 +    This only works if ~~/ROOTS is extended by a session created with
     4.8 +      ./bin/isabelle build -d test/Tools/isac/ADDTESTS/session-get_theory/ -v -b Bar
     4.9 +    See https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00060.html.
    4.10 +  *}
    4.11 +  options [document = false]
    4.12 +  theories Bar

     5.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Sep 02 16:16:08 2013 +0200
     5.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Sep 13 18:57:11 2013 +0200
     5.3 @@ -24,6 +24,7 @@
     5.4    "ADDTESTS/course/phst11/T2_Rewriting"
     5.5    "ADDTESTS/course/phst11/T3_MathEngine"
     5.6    "ADDTESTS/file-depend/BuildC_Test"
     5.7 +  "ADDTESTS/session-get_theory/Foo"
     5.8  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*)
     5.9    "~~/test/Pure/Isar/Test_Parsers"
    5.10  (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/test/Tools/isac/Test_Theory.thy	Fri Sep 13 18:57:11 2013 +0200
     6.3 @@ -0,0 +1,63 @@
     6.4 +theory Test_Theory imports "~~/src/Tools/isac/Knowledge/Rational"
     6.5 +begin                                                                            
     6.6 +ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
     6.7 +(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
     6.8 +  requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)
     6.9 +
    6.10 +section {* code for copy & paste ===============================================================*}
    6.11 +ML {*
    6.12 +"~~~~~ fun , args:"; val () = ();
    6.13 +"~~~~~ and , args:"; val () = ();
    6.14 +
    6.15 +"~~~~~ to  return val:"; val () = ();
    6.16 +
    6.17 +*}
    6.18 +text {*
    6.19 +  declare [[show_types]] 
    6.20 +  declare [[show_sorts]]
    6.21 +  find_theorems "?a <= ?a"
    6.22 +  
    6.23 +  print_facts
    6.24 +  print_statement ""
    6.25 +  print_theory
    6.26 +*}
    6.27 +ML {*
    6.28 +(*========== inhibit exn WN130909 TODO =========================================================
    6.29 +============ inhibit exn WN130909 TODO ========================================================*)
    6.30 +(*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    6.31 +-.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
    6.32 +*}
    6.33 +
    6.34 +section {* =================================================================*}
    6.35 +ML {*
    6.36 +*} ML {*
    6.37 +*} ML {*
    6.38 +*} ML {*
    6.39 +*} ML {*
    6.40 +*} ML {*
    6.41 +*} ML {*
    6.42 +*}
    6.43 +section {* =================================================================*}
    6.44 +ML {*
    6.45 +*} ML {*
    6.46 +*} ML {*
    6.47 +*} ML {*
    6.48 +*} ML {*
    6.49 +*} ML {*
    6.50 +*} ML {*
    6.51 +*} ML {*
    6.52 +*}
    6.53 +section {* =================================================================*}
    6.54 +ML {*
    6.55 +*} ML {*
    6.56 +*} ML {*
    6.57 +*} ML {*
    6.58 +*} ML {*
    6.59 +*} ML {*
    6.60 +*} ML {*
    6.61 +*} ML {*
    6.62 +*}
    6.63 +
    6.64 +end
    6.65 +
    6.66 +