# HG changeset patch
# User wenzelm
# Date 1368383434 -7200
# Node ID 13fb5e4f2893ba8f7379ea36889337616e673638
# Parent  f6858bb224c975d30722e2cfefcad4b393b2dfda
prefer standard Isabelle/ML operations;

diff -r f6858bb224c9 -r 13fb5e4f2893 src/Tools/WWW_Find/Start_WWW_Find.thy
--- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 20:25:45 2013 +0200
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Sun May 12 20:30:34 2013 +0200
@@ -7,7 +7,7 @@
 ML {*
   Options.default_put_bool "show_question_marks" false;
   YXML_Find_Theorems.init ();
-  val port = OS.Process.getEnv "SCGIPORT" |> the |> Int.fromString |> the;
+  val port = Markup.parse_int (getenv "SCGIPORT");
   ScgiServer.server' 10 "/" port;
 *}