1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Mon Feb 11 14:39:04 2013 +0100
     1.3 @@ -0,0 +1,14 @@
     1.4 +(* Load this theory to start the WWW_Find server on port defined by environment
     1.5 +   variable "SCGIPORT". Used by the isabelle wwwfind tool.
     1.6 +*)
     1.7 +
     1.8 +theory Start_WWW_Find imports WWW_Find begin
     1.9 +
    1.10 +ML {*
    1.11 +  YXML_Find_Theorems.init ();
    1.12 +  val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
    1.13 +  ScgiServer.server' 10 "/" port;
    1.14 +*}
    1.15 +
    1.16 +end
    1.17 +

     2.1 --- a/src/Tools/WWW_Find/doc/design.tex	Sun Feb 10 22:07:56 2013 +0100
     2.2 +++ b/src/Tools/WWW_Find/doc/design.tex	Mon Feb 11 14:39:04 2013 +0100
     2.3 @@ -267,8 +267,6 @@
     2.4  print mode of Isabelle, but the form fields and page structure were manually 
     2.5  implemented.
     2.6  
     2.7 -The module is built by using a \texttt{ROOT.ML} file inside a heap that 
     2.8 -contains the theories to be searched.
     2.9  The server is started by calling \texttt{ScgiServer.server}.
    2.10  Scripts have been created to automate this process.
    2.11  

     3.1 --- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Sun Feb 10 22:07:56 2013 +0100
     3.2 +++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon Feb 11 14:39:04 2013 +0100
     3.3 @@ -124,17 +124,20 @@
     3.4  
     3.5  WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
     3.6  SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
     3.7 -MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
     3.8 +
     3.9 +# inform theory which SCGI port to use via environment variable
    3.10 +export SCGIPORT
    3.11 +MLSTARTSERVER="use_thy \"Start_WWW_Find\";"
    3.12  
    3.13  case "$COMMAND" in
    3.14    start)
    3.15      "$LIGHTTPD" -f "$WWWCONFIG"
    3.16      if [ "$LOGFILE" = true ]; then
    3.17        (cd "$WWWFINDDIR"; \
    3.18 -       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" "$INPUT") &
    3.19 +       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" "$INPUT") &
    3.20      else
    3.21        (cd "$WWWFINDDIR"; \
    3.22 -       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" \
    3.23 +       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" \
    3.24           "$INPUT" > /dev/null 2> /dev/null) &
    3.25      fi
    3.26      ;;

     4.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Sun Feb 10 22:07:56 2013 +0100
     4.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Mon Feb 11 14:39:04 2013 +0100
     4.3 @@ -103,7 +103,7 @@
     4.4          loop ()
     4.5        end;
     4.6    in
     4.7 -    tracing ("SCGI server started.");
     4.8 +    tracing ("SCGI server started on port " ^ string_of_int port ^ ".");
     4.9      dump_handlers ();
    4.10      loop ();
    4.11      Socket.close passive_sock