more standard session setup for WWW_Find;

--- 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

--- /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
+

--- 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 ();
+

--- /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
+