# HG changeset patch
# User wenzelm
# Date 1343206502 -7200
# Node ID bf5b458701102a41f10d26423b7347db422423f4
# Parent  00eb5be9e76bf2b0e2a270e975dca49307c7413b
more standard session setup for WWW_Find;

diff -r 00eb5be9e76b -r bf5b45870110 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Jul 24 23:01:55 2012 +0200
+++ b/lib/scripts/getsettings	Wed Jul 25 10:55:02 2012 +0200
@@ -211,6 +211,16 @@
 
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
 
+#build condition etc.
+case "$ML_SYSTEM" in
+  polyml*)
+    ISABELLE_POLYML="true"
+    ;;
+  *)
+    ISABELLE_POLYML=""
+    ;;
+esac
+
 set +o allexport
 
 fi
diff -r 00eb5be9e76b -r bf5b45870110 src/Tools/WWW_Find/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/ROOT	Wed Jul 25 10:55:02 2012 +0200
@@ -0,0 +1,3 @@
+session WWW_Find in "." = Pure +
+  theories [condition = ISABELLE_POLYML] WWW_Find
+
diff -r 00eb5be9e76b -r bf5b45870110 src/Tools/WWW_Find/ROOT.ML
--- a/src/Tools/WWW_Find/ROOT.ML	Tue Jul 24 23:01:55 2012 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML	Wed Jul 25 10:55:02 2012 +0200
@@ -1,15 +1,3 @@
-if ML_System.is_polyml then
- (use "unicode_symbols.ML";
-  use "html_unicode.ML";
-  use "mime.ML";
-  use "http_status.ML";
-  use "http_util.ML";
-  use "xhtml.ML";
-  use "socket_util.ML";
-  use "scgi_req.ML";
-  use "scgi_server.ML";
-  use "echo.ML";
-  use "html_templates.ML";
-  use "find_theorems.ML";
-  use "yxml_find_theorems.ML")
+if ML_System.is_polyml then use_thy "WWW_Find"
 else ();
+
diff -r 00eb5be9e76b -r bf5b45870110 src/Tools/WWW_Find/WWW_Find.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/WWW_Find.thy	Wed Jul 25 10:55:02 2012 +0200
@@ -0,0 +1,20 @@
+theory WWW_Find
+imports Pure
+uses
+  "unicode_symbols.ML"
+  "html_unicode.ML"
+  "mime.ML"
+  "http_status.ML"
+  "http_util.ML"
+  "xhtml.ML"
+  "socket_util.ML"
+  "scgi_req.ML"
+  "scgi_server.ML"
+  "echo.ML"
+  "html_templates.ML"
+  "find_theorems.ML"
+  "yxml_find_theorems.ML"
+begin
+
+end
+