src/Tools/WWW_Find/Start_WWW_Find.thy
author wenzelm
Mon Feb 11 14:39:04 2013 +0100 (2013-02-11 ago)
changeset 51085 d90218288d51
child 51949 f6858bb224c9
permissions -rw-r--r--
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
wenzelm@51085
     1
(* Load this theory to start the WWW_Find server on port defined by environment
wenzelm@51085
     2
   variable "SCGIPORT". Used by the isabelle wwwfind tool.
wenzelm@51085
     3
*)
wenzelm@51085
     4
wenzelm@51085
     5
theory Start_WWW_Find imports WWW_Find begin
wenzelm@51085
     6
wenzelm@51085
     7
ML {*
wenzelm@51085
     8
  YXML_Find_Theorems.init ();
wenzelm@51085
     9
  val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
wenzelm@51085
    10
  ScgiServer.server' 10 "/" port;
wenzelm@51085
    11
*}
wenzelm@51085
    12
wenzelm@51085
    13
end
wenzelm@51085
    14