Re: [isabelle] RC3: patch to get wwwfind running again



On 12/02/13 00:17, Makarius wrote:
> On Mon, 11 Feb 2013, Rafal Kolanski wrote:
> 
>> So, here is a minimal patch to get the wwwfind tool working again. It
>> helps that there was nothing wrong with the code itself, only the way it
>> was being invoked.
> 
> I've looked only briefly, to understand what it does.  Should there be a
> static Start_WWW_Find.thy in the changeset?  It is missing.  (Or is it
> somehow dynamic?)

I apologise, I neglected to add it in the isabelle-release repository.
Here it is again.

Rafal Kolanski.

# HG changeset patch
# User Rafal Kolanski <rafal.kolanski at nicta.com.au>
# Date 1360588814 -39600
# Node ID 09fce1dd63877a85720152927ca8e03f9be8f4f8
# Parent  cbae5c5ffd234c591c8048b385fc35086d5ca2b7
Fix wwwfind tool startup.

diff --git a/src/Tools/WWW_Find/Start_WWW_Find.thy b/src/Tools/WWW_Find/Start_WWW_Find.thy
new file mode 100644
--- /dev/null
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy
@@ -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 --git a/src/Tools/WWW_Find/doc/design.tex b/src/Tools/WWW_Find/doc/design.tex
--- a/src/Tools/WWW_Find/doc/design.tex
+++ b/src/Tools/WWW_Find/doc/design.tex
@@ -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 --git a/src/Tools/WWW_Find/lib/Tools/wwwfind b/src/Tools/WWW_Find/lib/Tools/wwwfind
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind
@@ -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 --git a/src/Tools/WWW_Find/scgi_server.ML b/src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML
+++ b/src/Tools/WWW_Find/scgi_server.ML
@@ -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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.