1.1 --- a/lib/scripts/getsettings	Tue Jul 24 23:01:55 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Wed Jul 25 10:55:02 2012 +0200
     1.3 @@ -211,6 +211,16 @@
     1.4  
     1.5  ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
     1.6  
     1.7 +#build condition etc.
     1.8 +case "$ML_SYSTEM" in
     1.9 +  polyml*)
    1.10 +    ISABELLE_POLYML="true"
    1.11 +    ;;
    1.12 +  *)
    1.13 +    ISABELLE_POLYML=""
    1.14 +    ;;
    1.15 +esac
    1.16 +
    1.17  set +o allexport
    1.18  
    1.19  fi

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/WWW_Find/ROOT	Wed Jul 25 10:55:02 2012 +0200
     2.3 @@ -0,0 +1,3 @@
     2.4 +session WWW_Find in "." = Pure +
     2.5 +  theories [condition = ISABELLE_POLYML] WWW_Find
     2.6 +

     3.1 --- a/src/Tools/WWW_Find/ROOT.ML	Tue Jul 24 23:01:55 2012 +0200
     3.2 +++ b/src/Tools/WWW_Find/ROOT.ML	Wed Jul 25 10:55:02 2012 +0200
     3.3 @@ -1,15 +1,3 @@
     3.4 -if ML_System.is_polyml then
     3.5 - (use "unicode_symbols.ML";
     3.6 -  use "html_unicode.ML";
     3.7 -  use "mime.ML";
     3.8 -  use "http_status.ML";
     3.9 -  use "http_util.ML";
    3.10 -  use "xhtml.ML";
    3.11 -  use "socket_util.ML";
    3.12 -  use "scgi_req.ML";
    3.13 -  use "scgi_server.ML";
    3.14 -  use "echo.ML";
    3.15 -  use "html_templates.ML";
    3.16 -  use "find_theorems.ML";
    3.17 -  use "yxml_find_theorems.ML")
    3.18 +if ML_System.is_polyml then use_thy "WWW_Find"
    3.19  else ();
    3.20 +

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/WWW_Find/WWW_Find.thy	Wed Jul 25 10:55:02 2012 +0200
     4.3 @@ -0,0 +1,20 @@
     4.4 +theory WWW_Find
     4.5 +imports Pure
     4.6 +uses
     4.7 +  "unicode_symbols.ML"
     4.8 +  "html_unicode.ML"
     4.9 +  "mime.ML"
    4.10 +  "http_status.ML"
    4.11 +  "http_util.ML"
    4.12 +  "xhtml.ML"
    4.13 +  "socket_util.ML"
    4.14 +  "scgi_req.ML"
    4.15 +  "scgi_server.ML"
    4.16 +  "echo.ML"
    4.17 +  "html_templates.ML"
    4.18 +  "find_theorems.ML"
    4.19 +  "yxml_find_theorems.ML"
    4.20 +begin
    4.21 +
    4.22 +end
    4.23 +