# HG changeset patch
# User wenzelm
# Date 1360589944 -3600
# Node ID d90218288d517942cfbc80a6b2654ecb22735e5c
# Parent  cbae5c5ffd234c591c8048b385fc35086d5ca2b7
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

diff -r cbae5c5ffd23 -r d90218288d51 src/Tools/WWW_Find/Start_WWW_Find.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Mon Feb 11 14:39:04 2013 +0100
@@ -0,0 +1,14 @@
+(* Load this theory to start the WWW_Find server on port defined by environment
+   variable "SCGIPORT". Used by the isabelle wwwfind tool.
+*)
+
+theory Start_WWW_Find imports WWW_Find begin
+
+ML {*
+  YXML_Find_Theorems.init ();
+  val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
+  ScgiServer.server' 10 "/" port;
+*}
+
+end
+
diff -r cbae5c5ffd23 -r d90218288d51 src/Tools/WWW_Find/doc/design.tex
--- a/src/Tools/WWW_Find/doc/design.tex	Sun Feb 10 22:07:56 2013 +0100
+++ b/src/Tools/WWW_Find/doc/design.tex	Mon Feb 11 14:39:04 2013 +0100
@@ -267,8 +267,6 @@
 print mode of Isabelle, but the form fields and page structure were manually 
 implemented.
 
-The module is built by using a \texttt{ROOT.ML} file inside a heap that 
-contains the theories to be searched.
 The server is started by calling \texttt{ScgiServer.server}.
 Scripts have been created to automate this process.
 
diff -r cbae5c5ffd23 -r d90218288d51 src/Tools/WWW_Find/lib/Tools/wwwfind
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Sun Feb 10 22:07:56 2013 +0100
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon Feb 11 14:39:04 2013 +0100
@@ -124,17 +124,20 @@
 
 WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
 SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
-MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
+
+# inform theory which SCGI port to use via environment variable
+export SCGIPORT
+MLSTARTSERVER="use_thy \"Start_WWW_Find\";"
 
 case "$COMMAND" in
   start)
     "$LIGHTTPD" -f "$WWWCONFIG"
     if [ "$LOGFILE" = true ]; then
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" "$INPUT") &
+       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" "$INPUT") &
     else
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" \
+       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" \
          "$INPUT" > /dev/null 2> /dev/null) &
     fi
     ;;
diff -r cbae5c5ffd23 -r d90218288d51 src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML	Sun Feb 10 22:07:56 2013 +0100
+++ b/src/Tools/WWW_Find/scgi_server.ML	Mon Feb 11 14:39:04 2013 +0100
@@ -103,7 +103,7 @@
         loop ()
       end;
   in
-    tracing ("SCGI server started.");
+    tracing ("SCGI server started on port " ^ string_of_int port ^ ".");
     dump_handlers ();
     loop ();
     Socket.close passive_sock