# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1379091431 -7200
# Node ID cd5494eb08fd335f4c19f80bf1aa0afcebac8cbc
# Parent  c3f399ce32af17c516a14858d7360b7165fd3a10
Test_Theory without session Isac has limitations

diff -r c3f399ce32af -r cd5494eb08fd ROOTS
--- a/ROOTS	Mon Sep 02 16:16:08 2013 +0200
+++ b/ROOTS	Fri Sep 13 18:57:11 2013 +0200
@@ -10,4 +10,4 @@
 src/Sequents
 src/Doc
 src/Tools/isac
-
+test/Tools/isac/ADDTESTS/session-get_theory/
diff -r c3f399ce32af -r cd5494eb08fd test/Tools/isac/ADDTESTS/session-get_theory/Bar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/ADDTESTS/session-get_theory/Bar.thy	Fri Sep 13 18:57:11 2013 +0200
@@ -0,0 +1,5 @@
+theory Bar imports Pure begin
+ML {*
+  val bar_data = "bar_data"
+*}
+end
diff -r c3f399ce32af -r cd5494eb08fd test/Tools/isac/ADDTESTS/session-get_theory/Foo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/ADDTESTS/session-get_theory/Foo.thy	Fri Sep 13 18:57:11 2013 +0200
@@ -0,0 +1,9 @@
+theory Foo imports Bar begin
+ML {*
+  @{theory Bar};           (*OK                                                     *)
+(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)
+  case Thy_Info.lookup_theory "Bar" of
+    NONE => writeln "Expected, if Foo.thy is loaded directly. "
+  | SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar."
+*}
+end
diff -r c3f399ce32af -r cd5494eb08fd test/Tools/isac/ADDTESTS/session-get_theory/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/ADDTESTS/session-get_theory/ROOT	Fri Sep 13 18:57:11 2013 +0200
@@ -0,0 +1,9 @@
+session Bar in "~~/test/Tools/isac/ADDTESTS/session-get_theory" = Pure +
+  description {*
+    Trial to make the theory loader able to 'Thy_Info.get_theory "Bar"' in Foo.thy.
+    This only works if ~~/ROOTS is extended by a session created with
+      ./bin/isabelle build -d test/Tools/isac/ADDTESTS/session-get_theory/ -v -b Bar
+    See https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00060.html.
+  *}
+  options [document = false]
+  theories Bar
diff -r c3f399ce32af -r cd5494eb08fd test/Tools/isac/Test_Isac.thy
--- a/test/Tools/isac/Test_Isac.thy	Mon Sep 02 16:16:08 2013 +0200
+++ b/test/Tools/isac/Test_Isac.thy	Fri Sep 13 18:57:11 2013 +0200
@@ -24,6 +24,7 @@
   "ADDTESTS/course/phst11/T2_Rewriting"
   "ADDTESTS/course/phst11/T3_MathEngine"
   "ADDTESTS/file-depend/BuildC_Test"
+  "ADDTESTS/session-get_theory/Foo"
 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*)
   "~~/test/Pure/Isar/Test_Parsers"
 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
diff -r c3f399ce32af -r cd5494eb08fd test/Tools/isac/Test_Theory.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/Test_Theory.thy	Fri Sep 13 18:57:11 2013 +0200
@@ -0,0 +1,63 @@
+theory Test_Theory imports "~~/src/Tools/isac/Knowledge/Rational"
+begin                                                                            
+ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
+(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
+  requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)
+
+section {* code for copy & paste ===============================================================*}
+ML {*
+"~~~~~ fun , args:"; val () = ();
+"~~~~~ and , args:"; val () = ();
+
+"~~~~~ to  return val:"; val () = ();
+
+*}
+text {*
+  declare [[show_types]] 
+  declare [[show_sorts]]
+  find_theorems "?a <= ?a"
+  
+  print_facts
+  print_statement ""
+  print_theory
+*}
+ML {*
+(*========== inhibit exn WN130909 TODO =========================================================
+============ inhibit exn WN130909 TODO ========================================================*)
+(*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
+-.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
+*}
+
+section {* =================================================================*}
+ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*}
+section {* =================================================================*}
+ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*}
+section {* =================================================================*}
+ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*} ML {*
+*}
+
+end
+
+