retired wwwfind
authorkleing
Sat Apr 26 21:37:09 2014 +1000 (2014-04-26)
changeset 5673813b0fc4ece42
parent 56737 e4f363e16bdc
child 56739 0d56854096ba
retired wwwfind
NEWS
etc/components
src/Tools/ROOT
src/Tools/WWW_Find/Start_WWW_Find.thy
src/Tools/WWW_Find/WWW_Find.thy
src/Tools/WWW_Find/doc/README
src/Tools/WWW_Find/doc/design.tex
src/Tools/WWW_Find/echo.ML
src/Tools/WWW_Find/etc/settings
src/Tools/WWW_Find/etc/symbols
src/Tools/WWW_Find/find_theorems.ML
src/Tools/WWW_Find/html_templates.ML
src/Tools/WWW_Find/html_unicode.ML
src/Tools/WWW_Find/http_status.ML
src/Tools/WWW_Find/http_util.ML
src/Tools/WWW_Find/lib/Tools/wwwfind
src/Tools/WWW_Find/lighttpd.conf
src/Tools/WWW_Find/mime.ML
src/Tools/WWW_Find/scgi_req.ML
src/Tools/WWW_Find/scgi_server.ML
src/Tools/WWW_Find/socket_util.ML
src/Tools/WWW_Find/unicode_symbols.ML
src/Tools/WWW_Find/www/basic.css
src/Tools/WWW_Find/www/find_theorems.js
src/Tools/WWW_Find/www/pasting_help.html
src/Tools/WWW_Find/xhtml.ML
     1.1 --- a/NEWS	Sat Apr 26 06:43:06 2014 +0200
     1.2 +++ b/NEWS	Sat Apr 26 21:37:09 2014 +1000
     1.3 @@ -691,7 +691,8 @@
     1.4  incompatibility for old tools that do not use the $ISABELLE_PROCESS
     1.5  settings variable yet.
     1.6  
     1.7 -
     1.8 +* Retired the now unused Isabelle tool "wwwfind". Similar functionality
     1.9 +may be integrated into PIDE/jEdit at a later point.
    1.10  
    1.11  New in Isabelle2013-2 (December 2013)
    1.12  -------------------------------------
     2.1 --- a/etc/components	Sat Apr 26 06:43:06 2014 +0200
     2.2 +++ b/etc/components	Sat Apr 26 21:37:09 2014 +1000
     2.3 @@ -1,7 +1,6 @@
     2.4  src/Tools/Code
     2.5  src/Tools/jEdit
     2.6  src/Tools/Graphview
     2.7 -src/Tools/WWW_Find
     2.8  src/HOL/Mirabelle
     2.9  src/HOL/Mutabelle
    2.10  src/HOL/Library/Sum_of_Squares
     3.1 --- a/src/Tools/ROOT	Sat Apr 26 06:43:06 2014 +0200
     3.2 +++ b/src/Tools/ROOT	Sat Apr 26 21:37:09 2014 +1000
     3.3 @@ -1,6 +1,3 @@
     3.4 -session WWW_Find in WWW_Find = Pure +
     3.5 -  theories [condition = ISABELLE_POLYML] WWW_Find
     3.6 -
     3.7  session Spec_Check in Spec_Check = Pure +
     3.8    theories
     3.9      Spec_Check
     4.1 --- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Sat Apr 26 06:43:06 2014 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,13 +0,0 @@
     4.4 -(* Load this theory to start the WWW_Find server on port defined by environment
     4.5 -   variable "SCGIPORT". Used by the isabelle wwwfind tool.
     4.6 -*)
     4.7 -
     4.8 -theory Start_WWW_Find imports WWW_Find begin
     4.9 -
    4.10 -ML {*
    4.11 -  val port = Markup.parse_int (getenv "SCGIPORT");
    4.12 -  ScgiServer.server' 10 "/" port;
    4.13 -*}
    4.14 -
    4.15 -end
    4.16 -
     5.1 --- a/src/Tools/WWW_Find/WWW_Find.thy	Sat Apr 26 06:43:06 2014 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,19 +0,0 @@
     5.4 -theory WWW_Find
     5.5 -imports Pure
     5.6 -begin
     5.7 -
     5.8 -ML_file "unicode_symbols.ML"
     5.9 -ML_file "html_unicode.ML"
    5.10 -ML_file "mime.ML"
    5.11 -ML_file "http_status.ML"
    5.12 -ML_file "http_util.ML"
    5.13 -ML_file "xhtml.ML"
    5.14 -ML_file "socket_util.ML"
    5.15 -ML_file "scgi_req.ML"
    5.16 -ML_file "scgi_server.ML"
    5.17 -ML_file "echo.ML"
    5.18 -ML_file "html_templates.ML"
    5.19 -ML_file "find_theorems.ML"
    5.20 -
    5.21 -end
    5.22 -
     6.1 --- a/src/Tools/WWW_Find/doc/README	Sat Apr 26 06:43:06 2014 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,28 +0,0 @@
     6.4 -Requirements
     6.5 -------------
     6.6 -  lighttpd
     6.7 -  polyml (other ML systems untested)
     6.8 -
     6.9 -Quick setup
    6.10 ------------
    6.11 -*  install lighttpd if necessary
    6.12 -   (and optionally disable automatic startup on default www port)
    6.13 -
    6.14 -Quick instructions
    6.15 -------------------
    6.16 -* start the server with:
    6.17 -    isabelle wwwfind start
    6.18 -  (add -l for logging from ML)
    6.19 -
    6.20 -* connect (by default) on port 8000:
    6.21 -    http://localhost:8000/isabelle/find_theorems
    6.22 -
    6.23 -* test with the echo server:
    6.24 -    http://localhost:8000/isabelle/echo
    6.25 -
    6.26 -* check the status with:
    6.27 -    isabelle wwwfind status
    6.28 -
    6.29 -* stop the server with:
    6.30 -    isabelle wwwfind stop
    6.31 -
     7.1 --- a/src/Tools/WWW_Find/doc/design.tex	Sat Apr 26 06:43:06 2014 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,326 +0,0 @@
     7.4 -% vim:nojs: tw=76 sw=4 sts=4 fo=awn fdm=marker
     7.5 -%
     7.6 -% 20090406 T. Bourke
     7.7 -%	Original document.
     7.8 -%
     7.9 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    7.10 -\documentclass[a4paper,draft]{article} % XXX
    7.11 -%\documentclass[a4paper,final]{article}
    7.12 -% Preamble
    7.13 -\usepackage[T1]{fontenc}
    7.14 -\usepackage{textcomp}
    7.15 -\usepackage{ifdraft}
    7.16 -
    7.17 -\bibliographystyle{abbrv} % alpha
    7.18 -
    7.19 -\newcommand{\refsec}[1]{Section~\ref{sec:#1}}
    7.20 -\newcommand{\reffig}[1]{Figure~\ref{fig:#1}}
    7.21 -\newcommand{\reftab}[1]{Table~\ref{tab:#1}}
    7.22 -
    7.23 -%
    7.24 -\usepackage{acronym}
    7.25 -\usepackage{pst-all}
    7.26 -\usepackage{url}
    7.27 -
    7.28 -\title{Isabelle find\_theorems on the web}
    7.29 -\author{T. Bourke\thanks{NICTA}}
    7.30 -
    7.31 -\special{!/pdfmark where
    7.32 - {pop} {userdict /pdfmark /cleartomark load put} ifelse
    7.33 - [ /Author   (T. Bourke, NICTA)
    7.34 -   /Title    (IsabelleWWW: find_theorems
    7.35 -	      ($Date: 2008-10-03 16:09:02 +1000 (Fri, 03 Oct 2008) $))
    7.36 -   /Subject  (Web interface to find_theorems)
    7.37 -   /Keywords (isabelle, sml, http, www)
    7.38 -   /DOCINFO pdfmark}
    7.39 -
    7.40 -\begin{document}
    7.41 -% Title page and abstract
    7.42 -\maketitle
    7.43 -
    7.44 -\begin{abstract}
    7.45 -The Isabelle find\_theorems command processes queries against a theory 
    7.46 -database and returns a list of matching theorems.
    7.47 -It is usually given from the Proof General or command-line interface.
    7.48 -This document describes a web server implementation.
    7.49 -Two design alternatives are presented and an overview of an implementation 
    7.50 -of one is described.
    7.51 -\end{abstract}
    7.52 -
    7.53 -\section{Introduction}\label{sec:intro}
    7.54 -
    7.55 -This document describes the design and implementation of a web interface for 
    7.56 -the Isabelle find\_theorems command.
    7.57 -The design requirements and their consequences are detailed in \refsec{req}.
    7.58 -Two architectures were considered: \begin{enumerate}
    7.59 -
    7.60 -\item \emph{one process}: integrate a web server into Isabelle.
    7.61 -
    7.62 -\item \emph{two processes}: run Isabelle as a web server module.
    7.63 -
    7.64 -\end{enumerate}
    7.65 -A brief evaluation of the one process architecture is presented in 
    7.66 -\refsec{oneproc}.
    7.67 -An implementation of the two process is presented in \refsec{twoproc}.
    7.68 -
    7.69 -\section{Design requirements}\label{sec:req}
    7.70 -
    7.71 -The main requirements are:\begin{enumerate}
    7.72 -\item The system will allow users to search for theorems from a web browser.
    7.73 -\item It will allow queries across disparate Isabelle theories.
    7.74 -\item It will, at a minimum, handle theories from the L4.verified project.
    7.75 -\item It will run on a secure network.
    7.76 -\item There will be at most ten simultaneous users.
    7.77 -\end{enumerate}
    7.78 -
    7.79 -\noindent
    7.80 -Several \emph{a priori} choices are fixed:\begin{enumerate}
    7.81 -\item The search will run against an Isabelle heap.
    7.82 -\item A single heap will be built from the theories to be searched.
    7.83 -\item The system must be persistent, for two reasons: \begin{enumerate}
    7.84 -    \item Isabelle is slow to start against large heaps.
    7.85 -    \item Later enhancements may require tracking states at the server.
    7.86 -\end{enumerate}
    7.87 -\end{enumerate}
    7.88 -
    7.89 -\section{Evaluation: Isabelle web server}\label{sec:oneproc}
    7.90 -
    7.91 -The advantage of integrating a web server into Isabelle is that the 
    7.92 -find\_theorems service could be provided by a single process, which, in 
    7.93 -principle, would simplify administration.
    7.94 -Implementing even a simple \ac{HTTP} service from scratch is an unacceptable 
    7.95 -cost and fraught with potential problems and limitations.
    7.96 -It is preferable to adapt an existing system.
    7.97 -
    7.98 -As Isabelle is written in \ac{SML}, only \ac{HTTP} services also written in 
    7.99 -\ac{SML} can realistically be considered.
   7.100 -In principle Isabelle compiles on both Poly/ML and \ac{SML/NJ}, but in 
   7.101 -practice the former is faster, more widely used, and better supported.
   7.102 -In particular, the L4.verified project does not build effectively on 
   7.103 -\ac{SML/NJ}.
   7.104 -This further limits the potential to adapt an existing system.
   7.105 -
   7.106 -There are three \ac{SML} web server projects:\\
   7.107 -\centerline{\begin{tabular}{ll}
   7.108 -SMLServer &
   7.109 -    \url{http://www.smlserver.org}\\
   7.110 -FoxNet web server &
   7.111 -    \url{http://www.cs.cmu.edu/~fox/}\\
   7.112 -Swerve web server &
   7.113 -    \url{http://mlton.org/Swerve}
   7.114 -\end{tabular}}
   7.115 -
   7.116 -Unfortunately, none of these projects is suitable.
   7.117 -
   7.118 -The SMLServer is an Apache web server plugin.
   7.119 -It runs \ac{SML} programs that generate dynamic web pages.
   7.120 -SMLServer is based on the MLKit compiler.
   7.121 -It is unlikely that Isabelle and the l4.verified heaps could be compiled in 
   7.122 -MLKit, at least not without significant effort.
   7.123 -
   7.124 -The FoxNet web server was developed as part of the Fox project at \ac{CMU}.
   7.125 -The source is not readily available.
   7.126 -
   7.127 -The Swerve web server is part of an unpublished book on systems programming 
   7.128 -in \ac{SML}.
   7.129 -The source code is available and it is readily patched to run under the 
   7.130 -latest version of SML/NJ (110.67).
   7.131 -Adapting it to Poly/ML would require non-trivial effort because it is based 
   7.132 -on \ac{CML}, whose implementation on SML/NJ makes use of continuations 
   7.133 -(SMLofNJ.cont).
   7.134 -
   7.135 -\section{Implementation: Isabelle web module}\label{sec:twoproc}
   7.136 -
   7.137 -The description of the two process solution is divided into two subsections.
   7.138 -The first contains an overview of the architecture and web server specifics.
   7.139 -The second contains a summary of an \ac{SML} implementation of the web 
   7.140 -module in Isabelle.
   7.141 -
   7.142 -\subsection{Architecture and web server}\label{sec:oneproc:arch}
   7.143 -
   7.144 -\newcommand{\component}[1]{%
   7.145 -    \rput(0,0){\psframe(-.8,-.6)(.8,.6)}%
   7.146 -    \rput(0,0){\parbox{4.3em}{\centering{#1}}}}
   7.147 -
   7.148 -\begin{figure}
   7.149 -\centering%
   7.150 -\begin{pspicture}(-4.8,0)(3.3,4)%\psgrid
   7.151 -    \newpsstyle{conn}{arrows=->}%
   7.152 -    %
   7.153 -    \rput(-2.2,3.3){\component{web server}}%
   7.154 -    \rput( 2.2,3.3){\component{web module}}%
   7.155 -    \rput(-2.2,0.7){\component{web client}}%
   7.156 -    \rput(-4.2,3.4){%
   7.157 -	\psellipse(0,-.2)(.4,.2)%
   7.158 -	\psframe[linestyle=none,fillstyle=solid,fillcolor=white]%
   7.159 -		(-.4,-.2)(.4,.1)%
   7.160 -	\psellipse(0,.1)(.4,.2)%
   7.161 -	\psline(-.38,-.2)(-.38,.1)\psline(.38,-.2)(.38,.1)%
   7.162 -    }%
   7.163 -    \psline[style=conn,arrows=<->](-3.0,3.3)(-3.8,3.3)%
   7.164 -    %
   7.165 -    \rput[rB](3.3,2.15){server}%
   7.166 -    \psline[linestyle=dashed](-4.8,2)(3.3,2)%
   7.167 -    \rput[rt](3.3,1.90){network}%
   7.168 -    %
   7.169 -    \rput[B](0.0,3.55){\psframebox*{module protocol}}%
   7.170 -    \psline[style=conn](-1.4,3.4)(1.4,3.4)%
   7.171 -    \psline[style=conn](1.4,3.2)(-1.4,3.2)%
   7.172 -    %
   7.173 -    \rput[B]{90}(-2.4,2.0){\psframebox*{\ac{HTTP}}}%
   7.174 -    \psline[style=conn](-2.1,2.7)(-2.1,1.3)%
   7.175 -    \psline[style=conn](-2.3,1.3)(-2.3,2.7)%
   7.176 -\end{pspicture}
   7.177 -\caption{Overview of web module architecture\label{fig:modulearch}}
   7.178 -\end{figure}
   7.179 -
   7.180 -An overview of a simple web server architecture is presented in 
   7.181 -\reffig{modulearch}.
   7.182 -A \emph{web client} requests a \ac{URL} from a \emph{web server} over 
   7.183 -\ac{HTTP}.
   7.184 -The web server processes the request by fetching static elements from its 
   7.185 -local file system and communicating with \emph{web modules} to dynamically 
   7.186 -generate other elements.
   7.187 -The elements are sent back across the network to the web client.
   7.188 -
   7.189 -The web server communicates with web modules over a \emph{module protocol}, 
   7.190 -which dictates a means of passing requests and receiving responses.
   7.191 -There are several common module protocols.
   7.192 -
   7.193 -In the \ac{CGI}, the web server executes processes to service dynamic 
   7.194 -\acp{URL}.
   7.195 -Request details are placed in environment variables and sent on the standard 
   7.196 -input channels of processes, responses are read from the standard output 
   7.197 -channels of processes and transmitted back to web clients.
   7.198 -
   7.199 -The chief disadvantage of \ac{CGI} is that it creates a new process for 
   7.200 -every request.
   7.201 -Fast \ac{CGI} web modules, on the other hand, run persistently in a loop.
   7.202 -They receive and respond to web server requests over a duplex socket.
   7.203 -The Fast \ac{CGI} protocol is quite complicated.
   7.204 -There are, however, alternatives like \ac{SCGI} that are easier for web 
   7.205 -modules to support.
   7.206 -This is important when programming in \ac{SML} because both the number of 
   7.207 -developers and available libraries are small.
   7.208 -
   7.209 -An \ac{SCGI} web module listens on a socket for requests from a web server.
   7.210 -Requests are sent as stream of bytes.
   7.211 -The first part of the request is a null-delimited sequence of name and value 
   7.212 -pairs.
   7.213 -The second part is unparsed text sent from the web client.
   7.214 -The web module responds by sending text, usually \ac{HTTP} headers followed 
   7.215 -by \ac{HTML} data, back over the socket.
   7.216 -The whole protocol can be described in two 
   7.217 -pages.\footnote{\url{http://python.ca/scgi/protocol.txt}}
   7.218 -
   7.219 -Both the Apache and Lighttpd web servers support the \ac{SCGI} protocol.
   7.220 -Lighttpd was chosen because it seemed to be small, fast, and easy to 
   7.221 -configure.
   7.222 -Two settings are required to connect lighttpd to an \ac{SCGI} web module: 
   7.223 -\begin{verbatim}
   7.224 -server.modules = ( "mod_scgi" )
   7.225 -scgi.server = ("/isabelle" => ((
   7.226 -		  "host" => "127.0.0.1",
   7.227 -		  "port" => 64000,
   7.228 -		  "check-local" => "disable")))
   7.229 -\end{verbatim}
   7.230 -In this example, the \texttt{scgi.server} entry directs the web server to 
   7.231 -pass all \acp{URL} beginning with \texttt{/isabelle} to the web module 
   7.232 -listening on port \texttt{64000}.
   7.233 -
   7.234 -\subsection{Implementation in \acs{SML}}\label{sec:oneproc:impl}
   7.235 -
   7.236 -\begin{table}
   7.237 -\begin{tabular}{lp{.70\textwidth}}
   7.238 -\textbf{Module}	     &	\textbf{Description}\\\hline
   7.239 -Mime		     &	Rudimentary support for mime types.\\
   7.240 -HttpStatus	     &	\ac{HTTP} header status codes.\\
   7.241 -HttpUtil	     &	Produce \ac{HTTP} headers and parse query strings.\\
   7.242 -Xhtml		     &	Rudimentary support for generating \ac{HTML}.\\
   7.243 -SocketUtil	     &	Routines from The Standard ML Basis Library
   7.244 -			book.\footnote{Chapter 10, Gansner and Reppy, 
   7.245 -			Cambridge University Press.}\\
   7.246 -\textbf{ScgiReq}     &	Parse \ac{SCGI} requests.\\
   7.247 -\textbf{ScgiServer}  &	\ac{SCGI} server event loop and dispatch.\\
   7.248 -\textbf{FindTheorems}&	\ac{HTML} interface to find\_theorems.
   7.249 -\end{tabular}
   7.250 -\caption{Web module implementation\label{tab:moduleimpl}}
   7.251 -\end{table}
   7.252 -
   7.253 -The find\_theorems web module is implemented in \ac{SML}.
   7.254 -It uses elements of the Pure library in Isabelle.
   7.255 -The program comprises the nine modules shown in \reftab{moduleimpl}.
   7.256 -The three most important ones are shown in bold: ScgiReq, ScgiServer, and 
   7.257 -FindTheorems.
   7.258 -
   7.259 -ScgiReq implements the client-side of the \ac{SCGI} protocol.
   7.260 -It maps a binary input stream into a request data type.
   7.261 -
   7.262 -ScgiServer is a generic, multi-threaded \ac{SCGI} request dispatcher.
   7.263 -It accepts \ac{SCGI} requests on a designated socket, selects an appropriate 
   7.264 -handler from an internal list, and calls the handler in a new thread.
   7.265 -
   7.266 -FindTheorems registers a handler with ScgiServer.
   7.267 -It parses \ac{SCGI}/\ac{HTTP} requests, calls the Isabelle find\_theorems 
   7.268 -function, and returns the results as \ac{HTML}.
   7.269 -The \ac{HTML} generation of individual theorems is handled by the \ac{HTML} 
   7.270 -print mode of Isabelle, but the form fields and page structure were manually 
   7.271 -implemented.
   7.272 -
   7.273 -The server is started by calling \texttt{ScgiServer.server}.
   7.274 -Scripts have been created to automate this process.
   7.275 -
   7.276 -\subsection{Handling symbols}\label{sec:unicode}
   7.277 -
   7.278 -Isabelle theorems are usually written in mathematical notation.
   7.279 -Internally, however, Isabelle only manipulates \acs{ASCII} strings.
   7.280 -Symbols are encoded by strings that begin with a backslash and contain a 
   7.281 -symbol name between angle braces, for example, the symbol~$\longrightarrow$ 
   7.282 -becomes~\verb+\<longrightarrow>+.
   7.283 -The existing Thy/Html module in the Isabelle Pure theory converts many of 
   7.284 -these symbols to \ac{HTML} entities.
   7.285 -Custom routines are required to convert the missing symbols to \ac{HTML} 
   7.286 -\emph{numeric character references}, which are the Unicode codepoints of 
   7.287 -symbols printed in decimal between \verb+&#+ and \verb+;+.
   7.288 -Further, other routines were required for converting \acs{UTF-8} encoded 
   7.289 -strings sent from web browsers into Isabelle's symbol encoding.
   7.290 -
   7.291 -Isabelle is distributed with a text file that maps Isabelle symbols to 
   7.292 -Unicode codepoints.
   7.293 -A module was written to parse this file into symbol tables that map back and 
   7.294 -forth between Isabelle symbols and Unicode codepoints, and also between 
   7.295 -Isabelle \acs{ASCII} abbreviations (like \verb+-->+ for $\longrightarrow$) 
   7.296 -and Unicode codepoints.
   7.297 -
   7.298 -The conversion from Isabelle symbols to \ac{HTML} numeric character 
   7.299 -references is handled by a new printing mode, which is based in large part 
   7.300 -on the existing \ac{HTML} printing mode.
   7.301 -The new mode is used in combination with the existing \texttt{xsymbol} mode, 
   7.302 -to ensure that Isabelle symbols are used instead of \acs{ASCII} 
   7.303 -abbreviations.
   7.304 -
   7.305 -The conversion from \acs{UTF-8} is handled by a custom routine.
   7.306 -Additionally, there is a JavaScript routine that converts from Isabelle 
   7.307 -symbol encodings to \acs{UTF-8}, so that users can conveniently view 
   7.308 -manually-entered or pasted mathematical characters in the web browser 
   7.309 -interface.
   7.310 -
   7.311 -\section{Abbreviations}\label{sec:abbr}
   7.312 -
   7.313 -\begin{acronym}[SML/NJ] % longest acronym here
   7.314 -    \acro{ASCII}{American Standard Code for Information Interchange}
   7.315 -    \acro{CGI}{Common Gateway Interface}
   7.316 -    \acro{CML}{Concurrent ML}
   7.317 -    \acro{CMU}{Carnegie Mellon University}
   7.318 -    \acro{HTML}{Hyper Text Markup Language}
   7.319 -    \acro{HTTP}{Hyper Text Transfer Protocol}
   7.320 -    \acro{ML}{Meta Language}
   7.321 -    \acro{SCGI}{Simple CGI}
   7.322 -    \acro{SML}{Standard ML}
   7.323 -    \acro{SML/NJ}{Standard ML of New Jersey}
   7.324 -    \acro{URL}{Universal Resource Locator}
   7.325 -    \acro{UTF-8}{8-bit Unicode Transformation Format}
   7.326 -    \acro{WWW}{World Wide Web}
   7.327 -\end{acronym}
   7.328 -
   7.329 -\end{document}
     8.1 --- a/src/Tools/WWW_Find/echo.ML	Sat Apr 26 06:43:06 2014 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,16 +0,0 @@
     8.4 -(*  Title:      Tools/WWW_Find/echo.ML
     8.5 -    Author:     Timothy Bourke, NICTA
     8.6 -
     8.7 -Install simple echo server.
     8.8 -*)
     8.9 -
    8.10 -local
    8.11 -fun echo (req, content, send) =
    8.12 -  (send (ScgiReq.show req);
    8.13 -   send "--payload-----\n";
    8.14 -   send (Byte.bytesToString content);
    8.15 -   send "\n--------------\n")
    8.16 -in
    8.17 -val () = ScgiServer.register ("echo", SOME Mime.plain, echo);
    8.18 -end;
    8.19 -
     9.1 --- a/src/Tools/WWW_Find/etc/settings	Sat Apr 26 06:43:06 2014 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,8 +0,0 @@
     9.4 -# -*- shell-script -*- :mode=shellscript:
     9.5 -
     9.6 -LIGHTTPD="/usr/sbin/lighttpd"
     9.7 -
     9.8 -WWWFINDDIR="$COMPONENT"
     9.9 -WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
    9.10 -
    9.11 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"
    10.1 --- a/src/Tools/WWW_Find/etc/symbols	Sat Apr 26 06:43:06 2014 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,357 +0,0 @@
    10.4 -# Default interpretation of some Isabelle symbols (outdated version for WWW_Find)
    10.5 -
    10.6 -\<zero>                 code: 0x01d7ec  group: digit
    10.7 -\<one>                  code: 0x01d7ed  group: digit
    10.8 -\<two>                  code: 0x01d7ee  group: digit
    10.9 -\<three>                code: 0x01d7ef  group: digit
   10.10 -\<four>                 code: 0x01d7f0  group: digit
   10.11 -\<five>                 code: 0x01d7f1  group: digit
   10.12 -\<six>                  code: 0x01d7f2  group: digit
   10.13 -\<seven>                code: 0x01d7f3  group: digit
   10.14 -\<eight>                code: 0x01d7f4  group: digit
   10.15 -\<nine>                 code: 0x01d7f5  group: digit
   10.16 -\<A>                    code: 0x01d49c  group: letter
   10.17 -\<B>                    code: 0x00212c  group: letter
   10.18 -\<C>                    code: 0x01d49e  group: letter
   10.19 -\<D>                    code: 0x01d49f  group: letter
   10.20 -\<E>                    code: 0x002130  group: letter
   10.21 -\<F>                    code: 0x002131  group: letter
   10.22 -\<G>                    code: 0x01d4a2  group: letter
   10.23 -\<H>                    code: 0x00210b  group: letter
   10.24 -\<I>                    code: 0x002110  group: letter
   10.25 -\<J>                    code: 0x01d4a5  group: letter
   10.26 -\<K>                    code: 0x01d4a6  group: letter
   10.27 -\<L>                    code: 0x002112  group: letter
   10.28 -\<M>                    code: 0x002133  group: letter
   10.29 -\<N>                    code: 0x01d4a9  group: letter
   10.30 -\<O>                    code: 0x01d4aa  group: letter
   10.31 -\<P>                    code: 0x01d4ab  group: letter
   10.32 -\<Q>                    code: 0x01d4ac  group: letter
   10.33 -\<R>                    code: 0x00211b  group: letter
   10.34 -\<S>                    code: 0x01d4ae  group: letter
   10.35 -\<T>                    code: 0x01d4af  group: letter
   10.36 -\<U>                    code: 0x01d4b0  group: letter
   10.37 -\<V>                    code: 0x01d4b1  group: letter
   10.38 -\<W>                    code: 0x01d4b2  group: letter
   10.39 -\<X>                    code: 0x01d4b3  group: letter
   10.40 -\<Y>                    code: 0x01d4b4  group: letter
   10.41 -\<Z>                    code: 0x01d4b5  group: letter
   10.42 -\<a>                    code: 0x01d5ba  group: letter
   10.43 -\<b>                    code: 0x01d5bb  group: letter
   10.44 -\<c>                    code: 0x01d5bc  group: letter
   10.45 -\<d>                    code: 0x01d5bd  group: letter
   10.46 -\<e>                    code: 0x01d5be  group: letter
   10.47 -\<f>                    code: 0x01d5bf  group: letter
   10.48 -\<g>                    code: 0x01d5c0  group: letter
   10.49 -\<h>                    code: 0x01d5c1  group: letter
   10.50 -\<i>                    code: 0x01d5c2  group: letter
   10.51 -\<j>                    code: 0x01d5c3  group: letter
   10.52 -\<k>                    code: 0x01d5c4  group: letter
   10.53 -\<l>                    code: 0x01d5c5  group: letter
   10.54 -\<m>                    code: 0x01d5c6  group: letter
   10.55 -\<n>                    code: 0x01d5c7  group: letter
   10.56 -\<o>                    code: 0x01d5c8  group: letter
   10.57 -\<p>                    code: 0x01d5c9  group: letter
   10.58 -\<q>                    code: 0x01d5ca  group: letter
   10.59 -\<r>                    code: 0x01d5cb  group: letter
   10.60 -\<s>                    code: 0x01d5cc  group: letter
   10.61 -\<t>                    code: 0x01d5cd  group: letter
   10.62 -\<u>                    code: 0x01d5ce  group: letter
   10.63 -\<v>                    code: 0x01d5cf  group: letter
   10.64 -\<w>                    code: 0x01d5d0  group: letter
   10.65 -\<x>                    code: 0x01d5d1  group: letter
   10.66 -\<y>                    code: 0x01d5d2  group: letter
   10.67 -\<z>                    code: 0x01d5d3  group: letter
   10.68 -\<AA>                   code: 0x01d504  group: letter
   10.69 -\<BB>                   code: 0x01d505  group: letter
   10.70 -\<CC>                   code: 0x00212d  group: letter
   10.71 -\<DD>                   code: 0x01d507  group: letter
   10.72 -\<EE>                   code: 0x01d508  group: letter
   10.73 -\<FF>                   code: 0x01d509  group: letter
   10.74 -\<GG>                   code: 0x01d50a  group: letter
   10.75 -\<HH>                   code: 0x00210c  group: letter
   10.76 -\<II>                   code: 0x002111  group: letter
   10.77 -\<JJ>                   code: 0x01d50d  group: letter
   10.78 -\<KK>                   code: 0x01d50e  group: letter
   10.79 -\<LL>                   code: 0x01d50f  group: letter
   10.80 -\<MM>                   code: 0x01d510  group: letter
   10.81 -\<NN>                   code: 0x01d511  group: letter
   10.82 -\<OO>                   code: 0x01d512  group: letter
   10.83 -\<PP>                   code: 0x01d513  group: letter
   10.84 -\<QQ>                   code: 0x01d514  group: letter
   10.85 -\<RR>                   code: 0x00211c  group: letter
   10.86 -\<SS>                   code: 0x01d516  group: letter
   10.87 -\<TT>                   code: 0x01d517  group: letter
   10.88 -\<UU>                   code: 0x01d518  group: letter
   10.89 -\<VV>                   code: 0x01d519  group: letter
   10.90 -\<WW>                   code: 0x01d51a  group: letter
   10.91 -\<XX>                   code: 0x01d51b  group: letter
   10.92 -\<YY>                   code: 0x01d51c  group: letter
   10.93 -\<ZZ>                   code: 0x002128  group: letter
   10.94 -\<aa>                   code: 0x01d51e  group: letter
   10.95 -\<bb>                   code: 0x01d51f  group: letter
   10.96 -\<cc>                   code: 0x01d520  group: letter
   10.97 -\<dd>                   code: 0x01d521  group: letter
   10.98 -\<ee>                   code: 0x01d522  group: letter
   10.99 -\<ff>                   code: 0x01d523  group: letter
  10.100 -\<gg>                   code: 0x01d524  group: letter
  10.101 -\<hh>                   code: 0x01d525  group: letter
  10.102 -\<ii>                   code: 0x01d526  group: letter
  10.103 -\<jj>                   code: 0x01d527  group: letter
  10.104 -\<kk>                   code: 0x01d528  group: letter
  10.105 -\<ll>                   code: 0x01d529  group: letter
  10.106 -\<mm>                   code: 0x01d52a  group: letter
  10.107 -\<nn>                   code: 0x01d52b  group: letter
  10.108 -\<oo>                   code: 0x01d52c  group: letter
  10.109 -\<pp>                   code: 0x01d52d  group: letter
  10.110 -\<qq>                   code: 0x01d52e  group: letter
  10.111 -\<rr>                   code: 0x01d52f  group: letter
  10.112 -\<ss>                   code: 0x01d530  group: letter
  10.113 -\<tt>                   code: 0x01d531  group: letter
  10.114 -\<uu>                   code: 0x01d532  group: letter
  10.115 -\<vv>                   code: 0x01d533  group: letter
  10.116 -\<ww>                   code: 0x01d534  group: letter
  10.117 -\<xx>                   code: 0x01d535  group: letter
  10.118 -\<yy>                   code: 0x01d536  group: letter
  10.119 -\<zz>                   code: 0x01d537  group: letter
  10.120 -\<alpha>                code: 0x0003b1  group: greek
  10.121 -\<beta>                 code: 0x0003b2  group: greek
  10.122 -\<gamma>                code: 0x0003b3  group: greek
  10.123 -\<delta>                code: 0x0003b4  group: greek
  10.124 -\<epsilon>              code: 0x0003b5  group: greek
  10.125 -\<zeta>                 code: 0x0003b6  group: greek
  10.126 -\<eta>                  code: 0x0003b7  group: greek
  10.127 -\<theta>                code: 0x0003b8  group: greek
  10.128 -\<iota>                 code: 0x0003b9  group: greek
  10.129 -\<kappa>                code: 0x0003ba  group: greek
  10.130 -\<lambda>               code: 0x0003bb  group: greek  abbrev: %
  10.131 -\<mu>                   code: 0x0003bc  group: greek
  10.132 -\<nu>                   code: 0x0003bd  group: greek
  10.133 -\<xi>                   code: 0x0003be  group: greek
  10.134 -\<pi>                   code: 0x0003c0  group: greek
  10.135 -\<rho>                  code: 0x0003c1  group: greek
  10.136 -\<sigma>                code: 0x0003c3  group: greek
  10.137 -\<tau>                  code: 0x0003c4  group: greek
  10.138 -\<upsilon>              code: 0x0003c5  group: greek
  10.139 -\<phi>                  code: 0x0003c6  group: greek
  10.140 -\<chi>                  code: 0x0003c7  group: greek
  10.141 -\<psi>                  code: 0x0003c8  group: greek
  10.142 -\<omega>                code: 0x0003c9  group: greek
  10.143 -\<Gamma>                code: 0x000393  group: greek
  10.144 -\<Delta>                code: 0x000394  group: greek
  10.145 -\<Theta>                code: 0x000398  group: greek
  10.146 -\<Lambda>               code: 0x00039b  group: greek
  10.147 -\<Xi>                   code: 0x00039e  group: greek
  10.148 -\<Pi>                   code: 0x0003a0  group: greek
  10.149 -\<Sigma>                code: 0x0003a3  group: greek
  10.150 -\<Upsilon>              code: 0x0003a5  group: greek
  10.151 -\<Phi>                  code: 0x0003a6  group: greek
  10.152 -\<Psi>                  code: 0x0003a8  group: greek
  10.153 -\<Omega>                code: 0x0003a9  group: greek
  10.154 -\<bool>                 code: 0x01d539  group: letter
  10.155 -\<complex>              code: 0x002102  group: letter
  10.156 -\<nat>                  code: 0x002115  group: letter
  10.157 -\<rat>                  code: 0x00211a  group: letter
  10.158 -\<real>                 code: 0x00211d  group: letter
  10.159 -\<int>                  code: 0x002124  group: letter
  10.160 -\<leftarrow>            code: 0x002190  group: arrow
  10.161 -\<longleftarrow>        code: 0x0027f5  group: arrow
  10.162 -\<rightarrow>           code: 0x002192  group: arrow  abbrev: ->
  10.163 -\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: -->
  10.164 -\<Leftarrow>            code: 0x0021d0  group: arrow
  10.165 -\<Longleftarrow>        code: 0x0027f8  group: arrow
  10.166 -\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
  10.167 -\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
  10.168 -\<leftrightarrow>       code: 0x002194  group: arrow
  10.169 -\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->
  10.170 -\<Leftrightarrow>       code: 0x0021d4  group: arrow
  10.171 -\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>
  10.172 -\<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
  10.173 -\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
  10.174 -\<midarrow>             code: 0x002500  group: arrow
  10.175 -\<Midarrow>             code: 0x002550  group: arrow
  10.176 -\<hookleftarrow>        code: 0x0021a9  group: arrow
  10.177 -\<hookrightarrow>       code: 0x0021aa  group: arrow
  10.178 -\<leftharpoondown>      code: 0x0021bd  group: arrow
  10.179 -\<rightharpoondown>     code: 0x0021c1  group: arrow
  10.180 -\<leftharpoonup>        code: 0x0021bc  group: arrow
  10.181 -\<rightharpoonup>       code: 0x0021c0  group: arrow
  10.182 -\<rightleftharpoons>    code: 0x0021cc  group: arrow
  10.183 -\<leadsto>              code: 0x00219d  group: arrow  abbrev: ~>
  10.184 -\<downharpoonleft>      code: 0x0021c3  group: arrow
  10.185 -\<downharpoonright>     code: 0x0021c2  group: arrow
  10.186 -\<upharpoonleft>        code: 0x0021bf  group: arrow
  10.187 -#\<upharpoonright>       code: 0x0021be  group: arrow
  10.188 -\<restriction>          code: 0x0021be  group: punctuation
  10.189 -\<Colon>                code: 0x002237  group: punctuation
  10.190 -\<up>                   code: 0x002191  group: arrow
  10.191 -\<Up>                   code: 0x0021d1  group: arrow
  10.192 -\<down>                 code: 0x002193  group: arrow
  10.193 -\<Down>                 code: 0x0021d3  group: arrow
  10.194 -\<updown>               code: 0x002195  group: arrow
  10.195 -\<Updown>               code: 0x0021d5  group: arrow
  10.196 -\<langle>               code: 0x0027e8  group: punctuation  abbrev: <.
  10.197 -\<rangle>               code: 0x0027e9  group: punctuation  abbrev: .>
  10.198 -\<lceil>                code: 0x002308  group: punctuation
  10.199 -\<rceil>                code: 0x002309  group: punctuation
  10.200 -\<lfloor>               code: 0x00230a  group: punctuation
  10.201 -\<rfloor>               code: 0x00230b  group: punctuation
  10.202 -\<lparr>                code: 0x002987  group: punctuation  abbrev: (|
  10.203 -\<rparr>                code: 0x002988  group: punctuation  abbrev: |)
  10.204 -\<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
  10.205 -\<rbrakk>               code: 0x0027e7  group: punctuation  abbrev: |]
  10.206 -\<lbrace>               code: 0x002983  group: punctuation  abbrev: {.
  10.207 -\<rbrace>               code: 0x002984  group: punctuation  abbrev: .}
  10.208 -\<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
  10.209 -\<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
  10.210 -\<bottom>               code: 0x0022a5  group: logic
  10.211 -\<top>                  code: 0x0022a4  group: logic
  10.212 -\<and>                  code: 0x002227  group: logic  abbrev: /\
  10.213 -\<And>                  code: 0x0022c0  group: logic  abbrev: !!
  10.214 -\<or>                   code: 0x002228  group: logic  abbrev: \/
  10.215 -\<Or>                   code: 0x0022c1  group: logic  abbrev: ??
  10.216 -\<forall>               code: 0x002200  group: logic  abbrev: !
  10.217 -\<exists>               code: 0x002203  group: logic  abbrev: ?
  10.218 -\<nexists>              code: 0x002204  group: logic  abbrev: ~?
  10.219 -\<not>                  code: 0x0000ac  group: logic  abbrev: ~
  10.220 -\<box>                  code: 0x0025a1  group: logic
  10.221 -\<diamond>              code: 0x0025c7  group: logic
  10.222 -\<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
  10.223 -\<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
  10.224 -\<tturnstile>           code: 0x0022a9  group: relation  abbrev: ||-
  10.225 -\<TTurnstile>           code: 0x0022ab  group: relation  abbrev: ||=
  10.226 -\<stileturn>            code: 0x0022a3  group: relation  abbrev: -|
  10.227 -\<surd>                 code: 0x00221a  group: relation
  10.228 -\<le>                   code: 0x002264  group: relation  abbrev: <=
  10.229 -\<ge>                   code: 0x002265  group: relation  abbrev: >=
  10.230 -\<lless>                code: 0x00226a  group: relation
  10.231 -\<ggreater>             code: 0x00226b  group: relation
  10.232 -\<lesssim>              code: 0x002272  group: relation
  10.233 -\<greatersim>           code: 0x002273  group: relation
  10.234 -\<lessapprox>           code: 0x002a85  group: relation
  10.235 -\<greaterapprox>        code: 0x002a86  group: relation
  10.236 -\<in>                   code: 0x002208  group: relation  abbrev: :
  10.237 -\<notin>                code: 0x002209  group: relation  abbrev: ~:
  10.238 -\<subset>               code: 0x002282  group: relation
  10.239 -\<supset>               code: 0x002283  group: relation
  10.240 -\<subseteq>             code: 0x002286  group: relation  abbrev: (=
  10.241 -\<supseteq>             code: 0x002287  group: relation  abbrev: =)
  10.242 -\<sqsubset>             code: 0x00228f  group: relation
  10.243 -\<sqsupset>             code: 0x002290  group: relation
  10.244 -\<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
  10.245 -\<sqsupseteq>           code: 0x002292  group: relation  abbrev: =]
  10.246 -\<inter>                code: 0x002229  group: operator
  10.247 -\<Inter>                code: 0x0022c2  group: operator
  10.248 -\<union>                code: 0x00222a  group: operator
  10.249 -\<Union>                code: 0x0022c3  group: operator
  10.250 -\<squnion>              code: 0x002294  group: operator
  10.251 -\<Squnion>              code: 0x002a06  group: operator
  10.252 -\<sqinter>              code: 0x002293  group: operator
  10.253 -\<Sqinter>              code: 0x002a05  group: operator
  10.254 -\<setminus>             code: 0x002216  group: operator
  10.255 -\<propto>               code: 0x00221d  group: operator
  10.256 -\<uplus>                code: 0x00228e  group: operator
  10.257 -\<Uplus>                code: 0x002a04  group: operator
  10.258 -\<noteq>                code: 0x002260  group: relation  abbrev: ~=
  10.259 -\<sim>                  code: 0x00223c  group: relation
  10.260 -\<doteq>                code: 0x002250  group: relation
  10.261 -\<simeq>                code: 0x002243  group: relation
  10.262 -\<approx>               code: 0x002248  group: relation
  10.263 -\<asymp>                code: 0x00224d  group: relation
  10.264 -\<cong>                 code: 0x002245  group: relation
  10.265 -\<smile>                code: 0x002323  group: relation
  10.266 -\<equiv>                code: 0x002261  group: relation  abbrev: ==
  10.267 -\<frown>                code: 0x002322  group: relation
  10.268 -\<Join>                 code: 0x0022c8
  10.269 -\<bowtie>               code: 0x002a1d
  10.270 -\<prec>                 code: 0x00227a  group: relation
  10.271 -\<succ>                 code: 0x00227b  group: relation
  10.272 -\<preceq>               code: 0x00227c  group: relation
  10.273 -\<succeq>               code: 0x00227d  group: relation
  10.274 -\<parallel>             code: 0x002225  group: punctuation  abbrev: ||
  10.275 -\<bar>                  code: 0x0000a6  group: punctuation
  10.276 -\<plusminus>            code: 0x0000b1  group: operator
  10.277 -\<minusplus>            code: 0x002213  group: operator
  10.278 -\<times>                code: 0x0000d7  group: operator
  10.279 -\<div>                  code: 0x0000f7  group: operator
  10.280 -\<cdot>                 code: 0x0022c5  group: operator
  10.281 -\<star>                 code: 0x0022c6  group: operator
  10.282 -\<bullet>               code: 0x002219  group: operator
  10.283 -\<circ>                 code: 0x002218  group: operator
  10.284 -\<dagger>               code: 0x002020
  10.285 -\<ddagger>              code: 0x002021
  10.286 -\<lhd>                  code: 0x0022b2  group: relation
  10.287 -\<rhd>                  code: 0x0022b3  group: relation
  10.288 -\<unlhd>                code: 0x0022b4  group: relation
  10.289 -\<unrhd>                code: 0x0022b5  group: relation
  10.290 -\<triangleleft>         code: 0x0025c3  group: relation
  10.291 -\<triangleright>        code: 0x0025b9  group: relation
  10.292 -\<triangle>             code: 0x0025b3  group: relation
  10.293 -\<triangleq>            code: 0x00225c  group: relation
  10.294 -\<oplus>                code: 0x002295  group: operator  abbrev: +o
  10.295 -\<Oplus>                code: 0x002a01  group: operator  abbrev: +O
  10.296 -\<otimes>               code: 0x002297  group: operator  abbrev: *o
  10.297 -\<Otimes>               code: 0x002a02  group: operator  abbrev: *O
  10.298 -\<odot>                 code: 0x002299  group: operator  abbrev: .o
  10.299 -\<Odot>                 code: 0x002a00  group: operator  abbrev: .O
  10.300 -\<ominus>               code: 0x002296  group: operator  abbrev: -o
  10.301 -\<oslash>               code: 0x002298  group: operator  abbrev: /o
  10.302 -\<dots>                 code: 0x002026  group: punctuation abbrev: ...
  10.303 -\<cdots>                code: 0x0022ef  group: punctuation
  10.304 -\<Sum>                  code: 0x002211  group: operator  abbrev: SUM
  10.305 -\<Prod>                 code: 0x00220f  group: operator  abbrev: PROD
  10.306 -\<Coprod>               code: 0x002210  group: operator
  10.307 -\<infinity>             code: 0x00221e
  10.308 -\<integral>             code: 0x00222b  group: operator
  10.309 -\<ointegral>            code: 0x00222e  group: operator
  10.310 -\<clubsuit>             code: 0x002663
  10.311 -\<diamondsuit>          code: 0x002662
  10.312 -\<heartsuit>            code: 0x002661
  10.313 -\<spadesuit>            code: 0x002660
  10.314 -\<aleph>                code: 0x002135
  10.315 -\<emptyset>             code: 0x002205
  10.316 -\<nabla>                code: 0x002207
  10.317 -\<partial>              code: 0x002202
  10.318 -\<flat>                 code: 0x00266d
  10.319 -\<natural>              code: 0x00266e
  10.320 -\<sharp>                code: 0x00266f
  10.321 -\<angle>                code: 0x002220
  10.322 -\<copyright>            code: 0x0000a9
  10.323 -\<registered>           code: 0x0000ae
  10.324 -\<hyphen>               code: 0x0000ad  group: punctuation
  10.325 -\<inverse>              code: 0x0000af  group: punctuation
  10.326 -\<onequarter>           code: 0x0000bc  group: digit
  10.327 -\<onehalf>              code: 0x0000bd  group: digit
  10.328 -\<threequarters>        code: 0x0000be  group: digit
  10.329 -\<ordfeminine>          code: 0x0000aa
  10.330 -\<ordmasculine>         code: 0x0000ba
  10.331 -\<section>              code: 0x0000a7
  10.332 -\<paragraph>            code: 0x0000b6
  10.333 -\<exclamdown>           code: 0x0000a1
  10.334 -\<questiondown>         code: 0x0000bf
  10.335 -\<euro>                 code: 0x0020ac
  10.336 -\<pounds>               code: 0x0000a3
  10.337 -\<yen>                  code: 0x0000a5
  10.338 -\<cent>                 code: 0x0000a2
  10.339 -\<currency>             code: 0x0000a4
  10.340 -\<degree>               code: 0x0000b0
  10.341 -\<amalg>                code: 0x002a3f  group: operator
  10.342 -\<mho>                  code: 0x002127  group: operator
  10.343 -\<lozenge>              code: 0x0025ca
  10.344 -\<wp>                   code: 0x002118
  10.345 -\<wrong>                code: 0x002240  group: relation
  10.346 -\<struct>               code: 0x0022c4
  10.347 -\<acute>                code: 0x0000b4
  10.348 -\<index>                code: 0x000131
  10.349 -\<dieresis>             code: 0x0000a8
  10.350 -\<cedilla>              code: 0x0000b8
  10.351 -\<hungarumlaut>         code: 0x0002dd
  10.352 -\<some>                 code: 0x0003f5
  10.353 -\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
  10.354 -\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
  10.355 -\<^bold>                code: 0x002759  group: control  font: IsabelleText
  10.356 -\<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
  10.357 -\<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
  10.358 -\<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
  10.359 -\<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
  10.360 -
    11.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Sat Apr 26 06:43:06 2014 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,56 +0,0 @@
    11.4 -(*  Title:      Tools/WWW_Find/find_theorems.ML
    11.5 -    Author:     Timothy Bourke, NICTA
    11.6 -
    11.7 -Simple find_theorems server.
    11.8 -*)
    11.9 -
   11.10 -local
   11.11 -
   11.12 -val default_limit = 20;
   11.13 -val all_thy_names = sort string_ord (Thy_Info.get_names ());
   11.14 -
   11.15 -fun app_index f xs = fold_index (fn x => K (f x)) xs ();
   11.16 -
   11.17 -fun find_theorems arg_data send =
   11.18 -  let
   11.19 -    val args = Symtab.lookup arg_data;
   11.20 -
   11.21 -    val query_str = the_default "" (args "query");
   11.22 -    fun get_query () = Find_Theorems.read_query Position.none query_str;
   11.23 -
   11.24 -    val limit = case args "limit" of
   11.25 -        NONE => default_limit
   11.26 -      | SOME str => the_default default_limit (Int.fromString str);
   11.27 -    val thy_name = the_default "Main" (args "theory");
   11.28 -    val with_dups = is_some (args "with_dups");
   11.29 -    
   11.30 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
   11.31 -
   11.32 -    fun do_find query =
   11.33 -      let
   11.34 -        val (othmslen, thms) =
   11.35 -          Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
   11.36 -          ||> rev;
   11.37 -      in
   11.38 -        Xhtml.write send
   11.39 -          (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
   11.40 -        if null thms then ()
   11.41 -        else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
   11.42 -               HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
   11.43 -      end;
   11.44 -  in
   11.45 -    send Xhtml.doctype_xhtml1_0_strict;
   11.46 -    Xhtml.write_enclosed send
   11.47 -      (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
   11.48 -      (fn send => 
   11.49 -        if query_str = "" then ()
   11.50 -        else
   11.51 -          do_find (get_query ())
   11.52 -          handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
   11.53 -  end;
   11.54 -in
   11.55 -
   11.56 -val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
   11.57 -
   11.58 -end;
   11.59 -
    12.1 --- a/src/Tools/WWW_Find/html_templates.ML	Sat Apr 26 06:43:06 2014 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,163 +0,0 @@
    12.4 -(*  Title:      Tools/WWW_Find/html_templates.ML
    12.5 -    Author:     Timothy Bourke, NICTA
    12.6 -
    12.7 -HTML Templates for find theorems server.
    12.8 -*)
    12.9 -
   12.10 -signature HTML_TEMPLATES =
   12.11 -sig
   12.12 -  val find_theorems_form: string -> (string option * int * bool * string list) -> Xhtml.tag
   12.13 -
   12.14 -  val header: string -> (string option * int * bool * string list) -> Xhtml.tag
   12.15 -  val error: string -> Xhtml.tag
   12.16 -  val find_theorems_table: Xhtml.tag
   12.17 -
   12.18 -  val find_theorems_summary: int option * int * string Symtab.table -> Xhtml.tag
   12.19 -  val html_thm: Proof.context -> (int * (Facts.ref * thm)) -> Xhtml.tag
   12.20 -end
   12.21 -
   12.22 -
   12.23 -structure HTML_Templates: HTML_TEMPLATES =
   12.24 -struct
   12.25 -
   12.26 -open Xhtml;
   12.27 -
   12.28 -fun find_theorems_form thy_name (query, limit, withdups, all_thy_names) =
   12.29 -  let
   12.30 -    val query_input =
   12.31 -      input (id "query", {
   12.32 -        name = "query",
   12.33 -        itype = TextInput { value = query, maxlength = NONE }});
   12.34 -
   12.35 -    val max_results = divele noid
   12.36 -      [
   12.37 -        label (noid, { for = "limit" }, "Max. results:"),
   12.38 -        input (id "limit",
   12.39 -          { name = "limit",
   12.40 -            itype = TextInput { value = SOME (string_of_int limit),
   12.41 -                                maxlength = NONE }})
   12.42 -      ];
   12.43 -
   12.44 -    val theories = divele noid
   12.45 -      [
   12.46 -        label (noid, { for = "theory" }, "Search in:"),
   12.47 -        select (id "theory", { name = "theory", value = SOME thy_name })
   12.48 -               all_thy_names
   12.49 -      ];
   12.50 -
   12.51 -    val with_dups = divele noid
   12.52 -      [
   12.53 -        label (noid, { for = "withdups" }, "Allow duplicates:"),
   12.54 -        input (id "withdups",
   12.55 -          { name = "withdups",
   12.56 -            itype = Checkbox { checked = withdups, value = SOME "true" }})
   12.57 -      ];
   12.58 -
   12.59 -    val help = divele (class "help")
   12.60 -      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
   12.61 -  in
   12.62 -    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
   12.63 -      [tag "fieldset" []
   12.64 -        [tag "legend" [] [text "find_theorems"],
   12.65 -         (add_script (OnKeyPress, "encodequery(this)")
   12.66 -          o add_script (OnChange, "encodequery(this)")
   12.67 -          o add_script (OnMouseUp, "encodequery(this)")) query_input,
   12.68 -         divele (class "settings") [ max_results, theories, with_dups, help ],
   12.69 -         divele (class "mainbuttons")
   12.70 -           [ reset_button (id "reset"), submit_button (id "submit") ]
   12.71 -        ]
   12.72 -      ]
   12.73 -  end;
   12.74 -
   12.75 -fun header thy_name args =
   12.76 -  html { lang = "en" } [
   12.77 -    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
   12.78 -         [script (noid, { script_type="text/javascript",
   12.79 -                          src="/find_theorems.js" })],
   12.80 -    add_script (OnLoad, "encodequery(document.getElementById('query'))")
   12.81 -      (body noid [
   12.82 -          h (noid, 1, "Theory " ^ thy_name),
   12.83 -          find_theorems_form thy_name args,
   12.84 -          divele noid []
   12.85 -         ])
   12.86 -  ];
   12.87 -
   12.88 -fun error msg = p ((class "error"), msg);
   12.89 -
   12.90 -val find_theorems_table =
   12.91 -  table (class "findtheorems")
   12.92 -    [
   12.93 -      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
   12.94 -      tbody noid []
   12.95 -    ];
   12.96 -
   12.97 -fun show_criterion (b, c) =
   12.98 -  let
   12.99 -    fun prfx s =
  12.100 -      let
  12.101 -        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
  12.102 -      in span (class c, v) end;
  12.103 -  in
  12.104 -    (case c of
  12.105 -      Find_Theorems.Name name => prfx ("name: " ^ quote name)
  12.106 -    | Find_Theorems.Intro => prfx "intro"
  12.107 -    | Find_Theorems.Elim => prfx "elim"
  12.108 -    | Find_Theorems.Dest => prfx "dest"
  12.109 -    | Find_Theorems.Solves => prfx "solves"
  12.110 -    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
  12.111 -    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
  12.112 -  end;
  12.113 -
  12.114 -fun find_theorems_summary (othmslen, thmslen, args) =
  12.115 -  let
  12.116 -    val args =
  12.117 -      (case othmslen of
  12.118 -         NONE => args
  12.119 -       | SOME l => Symtab.update ("limit", string_of_int l) args)
  12.120 -    val qargs = HttpUtil.make_query_string args;
  12.121 -
  12.122 -    val num_found_text =
  12.123 -      (case othmslen of
  12.124 -         NONE => text (string_of_int thmslen)
  12.125 -       | SOME l =>
  12.126 -           a { href = "find_theorems" ^
  12.127 -               (if qargs = "" then "" else "?" ^ qargs),
  12.128 -           text = string_of_int l })
  12.129 -    val found = [text "found ", num_found_text, text " theorems"] : tag list;
  12.130 -    val displayed =
  12.131 -      if is_some othmslen
  12.132 -      then " (" ^ string_of_int thmslen ^ " displayed)"
  12.133 -      else "";
  12.134 -  in
  12.135 -    table (class "findtheoremsquery")
  12.136 -      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
  12.137 -  end
  12.138 -
  12.139 -(* FIXME!?! *)
  12.140 -fun is_sorry thm =
  12.141 -  Thm.proof_of thm
  12.142 -  |> Proofterm.approximate_proof_body
  12.143 -  |> Proofterm.all_oracles_of
  12.144 -  |> exists (fn (x, _) => x = "Pure.skip_proof");
  12.145 -
  12.146 -fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
  12.147 -
  12.148 -fun html_thm ctxt (n, (thmref, thm)) =
  12.149 -  let
  12.150 -    val output_thm =
  12.151 -      Output.output o Pretty.string_of_margin 100 o
  12.152 -        Display.pretty_thm (Config.put show_question_marks false ctxt);
  12.153 -  in
  12.154 -    tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
  12.155 -      [
  12.156 -        tag' "td" (class "name")
  12.157 -          [span' (sorry_class thm)
  12.158 -             [raw_text (Facts.string_of_ref thmref)]
  12.159 -          ],
  12.160 -        tag' "td" (class "thm") [pre noid (output_thm thm)]
  12.161 -      ]
  12.162 -  end;
  12.163 -
  12.164 -end;
  12.165 -
  12.166 -
    13.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Sat Apr 26 06:43:06 2014 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,80 +0,0 @@
    13.4 -(*  Title:      Tools/WWW_Find/html_unicode.ML
    13.5 -    Author:     Timothy Bourke, NICTA
    13.6 -                Based on Pure/Thy/html.ML
    13.7 -                by Markus Wenzel and Stefan Berghofer, TU Muenchen
    13.8 -
    13.9 -HTML presentation elements that use unicode code points.
   13.10 -*)
   13.11 -
   13.12 -signature HTML_UNICODE =
   13.13 -sig
   13.14 -  val print_mode: ('a -> 'b) -> 'a -> 'b
   13.15 -end;
   13.16 -
   13.17 -structure HTML_Unicode: HTML_UNICODE =
   13.18 -struct
   13.19 -
   13.20 -(** HTML print modes **)
   13.21 -
   13.22 -(* mode *)
   13.23 -
   13.24 -val htmlunicodeN = "HTMLUnicode";
   13.25 -fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
   13.26 -
   13.27 -(* symbol output *)
   13.28 -
   13.29 -local
   13.30 -  val sym_width_lookup = Symtab.make
   13.31 -   [("\<Longleftarrow>", 2),
   13.32 -    ("\<longleftarrow>", 2),
   13.33 -    ("\<Longrightarrow>", 2),
   13.34 -    ("\<longrightarrow>", 2),
   13.35 -    ("\<longleftrightarrow>", 2),
   13.36 -    ("\<^bsub>", 0),
   13.37 -    ("\<^esub>", 0),
   13.38 -    ("\<^bsup>", 0),
   13.39 -    ("\<^esup>", 0)];
   13.40 -
   13.41 -  fun sym_width s =
   13.42 -    (case Symtab.lookup sym_width_lookup s of
   13.43 -       NONE => 1
   13.44 -     | SOME w => w);
   13.45 -
   13.46 -  fun output_sym s =
   13.47 -    if Symbol.is_raw s then (1, Symbol.decode_raw s)
   13.48 -    else
   13.49 -      (case UnicodeSymbols.symbol_to_unicode s of
   13.50 -         SOME x => (sym_width s, "&#" ^ string_of_int x ^ ";") (* numeric entities *)
   13.51 -         (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x])     (* utf-8 *) *)
   13.52 -       | NONE => (size s, XML.text s));
   13.53 -
   13.54 -  fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
   13.55 -  fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
   13.56 -
   13.57 -  fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
   13.58 -    | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
   13.59 -    | output_syms (s :: ss) = output_sym s :: output_syms ss
   13.60 -    | output_syms [] = [];
   13.61 -
   13.62 -  fun output_width str =
   13.63 -    if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
   13.64 -    then Output.default_output str
   13.65 -    else
   13.66 -      let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
   13.67 -        (output_syms (Symbol.explode str)) 0
   13.68 -      in (implode syms, width) end;
   13.69 -in
   13.70 -
   13.71 -val output = #1 o output_width;
   13.72 -
   13.73 -val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw;
   13.74 -
   13.75 -end;
   13.76 -
   13.77 -(* common markup *)
   13.78 -
   13.79 -fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
   13.80 -
   13.81 -val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name);
   13.82 -
   13.83 -end;
    14.1 --- a/src/Tools/WWW_Find/http_status.ML	Sat Apr 26 06:43:06 2014 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,158 +0,0 @@
    14.4 -(*  Title:      Tools/WWW_Find/http_status.ML
    14.5 -    Author:     Timothy Bourke, NICTA
    14.6 -
    14.7 -HTTP status codes and reasons.
    14.8 -*)
    14.9 -
   14.10 -signature HTTP_STATUS =
   14.11 -sig
   14.12 -  type t
   14.13 -
   14.14 -  val to_status_code : t -> int
   14.15 -  val to_reason : t -> string
   14.16 -  val from_status_code : int -> t option
   14.17 -
   14.18 -  val continue : t
   14.19 -  val switching_protocols : t
   14.20 -  val ok : t
   14.21 -  val created : t
   14.22 -  val accepted : t
   14.23 -  val non_authoritative_information : t
   14.24 -  val no_content : t
   14.25 -  val reset_content : t
   14.26 -  val partial_content : t
   14.27 -  val multiple_choices : t
   14.28 -  val moved_permanently : t
   14.29 -  val found : t
   14.30 -  val see_other : t
   14.31 -  val not_modified : t
   14.32 -  val use_proxy : t
   14.33 -  val temporary_redirect : t
   14.34 -  val bad_request : t
   14.35 -  val unauthorized : t
   14.36 -  val payment_required : t
   14.37 -  val forbidden : t
   14.38 -  val not_found : t
   14.39 -  val method_not_allowed : t
   14.40 -  val not_acceptable : t
   14.41 -  val proxy_authentication_required : t
   14.42 -  val request_timeout : t
   14.43 -  val conflict : t
   14.44 -  val gone : t
   14.45 -  val length_required : t
   14.46 -  val precondition_failed : t
   14.47 -  val request_entity_too_large : t
   14.48 -  val request_uri_too_long : t
   14.49 -  val unsupported_media_type : t
   14.50 -  val requested_range_not_satisfiable : t
   14.51 -  val expectation_failed : t
   14.52 -  val internal_server_error : t
   14.53 -  val not_implemented : t
   14.54 -  val bad_gateway : t
   14.55 -  val service_unavailable : t
   14.56 -  val gateway_timeout : t
   14.57 -  val http_version_not_supported : t
   14.58 -
   14.59 -end;
   14.60 -
   14.61 -structure HttpStatus : HTTP_STATUS =
   14.62 -struct
   14.63 -
   14.64 -type t = int
   14.65 -
   14.66 -local
   14.67 -val int_status_map = Inttab.make
   14.68 -  [(100, "Continue"),
   14.69 -   (101, "Switching Protocols"),
   14.70 -   (200, "OK"),
   14.71 -   (201, "Created"),
   14.72 -   (202, "Accepted"),
   14.73 -   (203, "Non-Authoritative Information"),
   14.74 -   (204, "No Content"),
   14.75 -   (205, "Reset Content"),
   14.76 -   (206, "Partial Content"),
   14.77 -   (300, "Multiple Choices"),
   14.78 -   (301, "Moved Permanently"),
   14.79 -   (302, "Found"),
   14.80 -   (303, "See Other"),
   14.81 -   (304, "Not Modified"),
   14.82 -   (305, "Use Proxy"),
   14.83 -   (307, "Temporary Redirect"),
   14.84 -   (400, "Bad Request"),
   14.85 -   (401, "Unauthorized"),
   14.86 -   (402, "Payment Required"),
   14.87 -   (403, "Forbidden"),
   14.88 -   (404, "Not Found"),
   14.89 -   (405, "Method Not Allowed"),
   14.90 -   (406, "Not Acceptable"),
   14.91 -   (407, "Proxy Authentication Required"),
   14.92 -   (408, "Request Timeout"),
   14.93 -   (409, "Conflict"),
   14.94 -   (410, "Gone"),
   14.95 -   (411, "Length Required"),
   14.96 -   (412, "Precondition Failed"),
   14.97 -   (413, "Request Entity Too Large"),
   14.98 -   (414, "Request URI Too Long"),
   14.99 -   (415, "Unsupported Media Type"),
  14.100 -   (416, "Requested Range Not Satisfiable"),
  14.101 -   (417, "Expectation Failed"),
  14.102 -   (500, "Internal Server Error"),
  14.103 -   (501, "Not Implemented"),
  14.104 -   (502, "Bad Gateway"),
  14.105 -   (503, "Service Unavailable"),
  14.106 -   (504, "Gateway Timeout"),
  14.107 -   (505, "HTTP Version Not Supported")];
  14.108 -in
  14.109 -fun from_status_code i =
  14.110 -  if is_some (Inttab.lookup int_status_map i)
  14.111 -  then SOME i
  14.112 -  else NONE;
  14.113 -
  14.114 -val to_reason = the o Inttab.lookup int_status_map;
  14.115 -end;
  14.116 -
  14.117 -val to_status_code = I;
  14.118 -
  14.119 -val continue = 100;
  14.120 -val switching_protocols = 101;
  14.121 -val ok = 200;
  14.122 -val created = 201;
  14.123 -val accepted = 202;
  14.124 -val non_authoritative_information = 203;
  14.125 -val no_content = 204;
  14.126 -val reset_content = 205;
  14.127 -val partial_content = 206;
  14.128 -val multiple_choices = 300;
  14.129 -val moved_permanently = 301;
  14.130 -val found = 302;
  14.131 -val see_other = 303;
  14.132 -val not_modified = 304;
  14.133 -val use_proxy = 305;
  14.134 -val temporary_redirect = 307;
  14.135 -val bad_request = 400;
  14.136 -val unauthorized = 401;
  14.137 -val payment_required = 402;
  14.138 -val forbidden = 403;
  14.139 -val not_found = 404;
  14.140 -val method_not_allowed = 405;
  14.141 -val not_acceptable = 406;
  14.142 -val proxy_authentication_required = 407;
  14.143 -val request_timeout = 408;
  14.144 -val conflict = 409;
  14.145 -val gone = 410;
  14.146 -val length_required = 411;
  14.147 -val precondition_failed = 412;
  14.148 -val request_entity_too_large = 413;
  14.149 -val request_uri_too_long = 414;
  14.150 -val unsupported_media_type = 415;
  14.151 -val requested_range_not_satisfiable = 416;
  14.152 -val expectation_failed = 417;
  14.153 -val internal_server_error = 500;
  14.154 -val not_implemented = 501;
  14.155 -val bad_gateway = 502;
  14.156 -val service_unavailable = 503;
  14.157 -val gateway_timeout = 504;
  14.158 -val http_version_not_supported = 505;
  14.159 -
  14.160 -end;
  14.161 -
    15.1 --- a/src/Tools/WWW_Find/http_util.ML	Sat Apr 26 06:43:06 2014 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,95 +0,0 @@
    15.4 -(*  Title:      Tools/WWW_Find/http_util.ML
    15.5 -    Author:     Timothy Bourke, NICTA
    15.6 -
    15.7 -Rudimentary utility functions for HTTP.
    15.8 -*)
    15.9 -
   15.10 -signature HTTP_UTIL =
   15.11 -sig
   15.12 -  val crlf : string
   15.13 -  val reply_header : HttpStatus.t * Mime.t option * (string * string) list -> string
   15.14 -  val parse_query_string : string -> string Symtab.table
   15.15 -  val make_query_string : string Symtab.table -> string
   15.16 -end;
   15.17 -
   15.18 -structure HttpUtil : HTTP_UTIL =
   15.19 -struct
   15.20 -
   15.21 -val crlf = "\r\n";
   15.22 -
   15.23 -fun make_header_field (name, value) = implode [name, ": ", value, crlf];
   15.24 -
   15.25 -fun reply_header (status, content_type, extra_fields) =
   15.26 -  let
   15.27 -    val code = (string_of_int o HttpStatus.to_status_code) status;
   15.28 -    val reason = HttpStatus.to_reason status;
   15.29 -    val show_content_type = pair "Content-Type" o Mime.show_type;
   15.30 -  in
   15.31 -  implode
   15.32 -    (map make_header_field
   15.33 -      (("Status", implode [code, " ", reason])
   15.34 -       :: (the_list o Option.map show_content_type) content_type
   15.35 -       @ extra_fields)
   15.36 -    @ [crlf])
   15.37 -  end;
   15.38 -
   15.39 -val split_fields = Substring.splitl (fn c => c <> #"=")
   15.40 -                   #> apsnd (Substring.triml 1);
   15.41 -
   15.42 -fun decode_url s =
   15.43 -  let
   15.44 -    fun to_char c =
   15.45 -      Substring.triml 1 c
   15.46 -      |> Int.scan StringCvt.HEX Substring.getc
   15.47 -      |> the
   15.48 -      |> fst
   15.49 -      |> Char.chr
   15.50 -      |> String.str
   15.51 -      |> Substring.full
   15.52 -      handle Option.Option => c;
   15.53 -
   15.54 -    fun f (done, s) =
   15.55 -      let
   15.56 -        val (pre, post) = Substring.splitl (Char.notContains "+%") s;
   15.57 -      in
   15.58 -        if Substring.isEmpty post
   15.59 -        then (Substring.concat o rev) (pre::done)
   15.60 -        else
   15.61 -          if Substring.first post = SOME #"+"
   15.62 -            (* Substring.isPrefix "+" post *)(* seg fault in Poly/ML 5.1 *)
   15.63 -          then f (Substring.full " "::pre::done, Substring.triml 1 post)
   15.64 -          else let
   15.65 -            val (c, rest) = Substring.splitAt (post, 3)
   15.66 -                            handle General.Subscript =>
   15.67 -                              (Substring.full "%25", Substring.triml 1 post);
   15.68 -          in f (to_char c::pre::done, rest) end
   15.69 -      end;
   15.70 -  in f ([], s) end;
   15.71 -
   15.72 -val parse_query_string =
   15.73 -  Substring.full
   15.74 -  #> Substring.tokens (Char.contains "&;")
   15.75 -  #> map split_fields
   15.76 -  #> map (pairself (UnicodeSymbols.utf8_to_symbols o decode_url))
   15.77 -  #> distinct ((op =) o pairself fst)
   15.78 -  #> Symtab.make;
   15.79 -
   15.80 -local
   15.81 -fun to_entity #" " = "+"
   15.82 -  | to_entity c =
   15.83 -      if Char.isAlphaNum c orelse Char.contains ".-~_" c
   15.84 -      then String.str c
   15.85 -      else "%" ^ Int.fmt StringCvt.HEX (Char.ord c);
   15.86 -in
   15.87 -val encode_url = Substring.translate to_entity o Substring.full;
   15.88 -end
   15.89 -
   15.90 -fun join_pairs (n, v) = encode_url n ^ "=" ^ encode_url v;
   15.91 -
   15.92 -val make_query_string =
   15.93 -  Symtab.dest
   15.94 -  #> map join_pairs
   15.95 -  #> space_implode "&";
   15.96 -
   15.97 -end;
   15.98 -
    16.1 --- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Sat Apr 26 06:43:06 2014 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,153 +0,0 @@
    16.4 -#!/usr/bin/env bash
    16.5 -#
    16.6 -# Author: Timothy Bourke, NICTA
    16.7 -#         Based on scripts by Makarius Wenzel, TU Muenchen
    16.8 -#
    16.9 -# DESCRIPTION: run find theorems web server
   16.10 - 
   16.11 -PRG=$(basename "$0")
   16.12 -
   16.13 -function usage()
   16.14 -{
   16.15 -  echo
   16.16 -  echo "Usage: $ISABELLE_TOOL $PRG [Command] [Options] [HEAP]"
   16.17 -  echo
   16.18 -  echo "  Command must be one of:"
   16.19 -  echo "    start        start lighttpd and isabelle"
   16.20 -  echo "    stop         stop lighttpd and isabelle"
   16.21 -  echo "    status       show www and scgi port statuses"
   16.22 -  echo
   16.23 -  echo "  Options are:"
   16.24 -  echo "    -l           make log file"
   16.25 -  echo "    -c           specify lighttpd config file"
   16.26 -  echo "                 (default: $WWWCONFIG)"
   16.27 -  echo
   16.28 -  echo "  Provide a web interface to find_theorems against the given HEAP"
   16.29 -  echo
   16.30 -  exit 1
   16.31 -}
   16.32 -
   16.33 -function fail()
   16.34 -{
   16.35 -  echo "$1" >&2
   16.36 -  exit 2
   16.37 -}
   16.38 -
   16.39 -function checkplatform()
   16.40 -{
   16.41 -  case "$ISABELLE_PLATFORM" in
   16.42 -    *-linux)
   16.43 -      ;;
   16.44 -    *)
   16.45 -      fail "Platform $ISABELLE_PLATFORM currently not supported by $PRG component"
   16.46 -      ;;
   16.47 -  esac
   16.48 -}
   16.49 -
   16.50 -function kill_by_port () {
   16.51 -  IPADDR='[0-9]*\.[0-9]*\.[0-9]*\.[0-9]*'
   16.52 -  PID=$(netstat -nltp 2>/dev/null \
   16.53 -        | sed -ne "s#^.*${IPADDR}:$1 *${IPADDR}:.*LISTEN *\([0-9]*\)/.*#\1#p")
   16.54 -  if [ "$PID" != "" ]; then
   16.55 -    kill -9 $PID
   16.56 -  fi
   16.57 -}
   16.58 -
   16.59 -function show_socket_status () {
   16.60 -  netstat -latp 2>/dev/null | grep ":$1 "
   16.61 -}
   16.62 -
   16.63 -## platform support check
   16.64 -
   16.65 -checkplatform
   16.66 -
   16.67 -## process command line
   16.68 -
   16.69 -case "$1" in
   16.70 -  start|stop|status)
   16.71 -    COMMAND="$1"
   16.72 -    ;;
   16.73 -  *)
   16.74 -    usage
   16.75 -    ;;
   16.76 -esac
   16.77 -
   16.78 -shift
   16.79 -
   16.80 -# options
   16.81 -
   16.82 -NO_OPTS=true
   16.83 -LOGFILE=false
   16.84 -
   16.85 -while getopts "lc:" OPT
   16.86 -do
   16.87 -  NO_OPTS=""
   16.88 -  case "$OPT" in
   16.89 -    l)
   16.90 -      LOGFILE=true
   16.91 -      ;;
   16.92 -    c)
   16.93 -      USER_CONFIG="$OPTARG"
   16.94 -      ;;
   16.95 -    \?)
   16.96 -      usage
   16.97 -      ;;
   16.98 -  esac
   16.99 -done
  16.100 -
  16.101 -shift $(($OPTIND - 1))
  16.102 -
  16.103 -# args
  16.104 -
  16.105 -INPUT=""
  16.106 -
  16.107 -if [ "$#" -ge 1 ]; then
  16.108 -  INPUT="$1"
  16.109 -  shift
  16.110 -fi
  16.111 -
  16.112 -[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
  16.113 -
  16.114 -[ -x "$LIGHTTPD" ] || fail "lighttpd not found at $LIGHTTPD"
  16.115 -
  16.116 -if [ -n "$USER_CONFIG" ]; then
  16.117 -  WWWCONFIG="$USER_CONFIG"
  16.118 -else
  16.119 -  TMP=$(mktemp "/tmp/lighttpd.conf.$$.XXX")
  16.120 -  echo "server.document-root = \"$WWWFINDDIR/www\"" > "$TMP"
  16.121 -  cat "$WWWCONFIG" >> "$TMP"
  16.122 -  WWWCONFIG="$TMP"
  16.123 -fi
  16.124 -
  16.125 -
  16.126 -## main
  16.127 -
  16.128 -WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
  16.129 -SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
  16.130 -
  16.131 -# inform theory which SCGI port to use via environment variable
  16.132 -export SCGIPORT
  16.133 -MLSTARTSERVER="use_thy \"Start_WWW_Find\";"
  16.134 -
  16.135 -case "$COMMAND" in
  16.136 -  start)
  16.137 -    "$LIGHTTPD" -f "$WWWCONFIG"
  16.138 -    if [ "$LOGFILE" = true ]; then
  16.139 -      (cd "$WWWFINDDIR"; \
  16.140 -       nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" "$INPUT") &
  16.141 -    else
  16.142 -      (cd "$WWWFINDDIR"; \
  16.143 -       nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" \
  16.144 -         "$INPUT" > /dev/null 2> /dev/null) &
  16.145 -    fi
  16.146 -    ;;
  16.147 -  stop)
  16.148 -    kill_by_port $SCGIPORT
  16.149 -    kill_by_port $WWWPORT
  16.150 -    ;;
  16.151 -  status)
  16.152 -    show_socket_status $WWWPORT
  16.153 -    show_socket_status $SCGIPORT
  16.154 -    ;;
  16.155 -esac
  16.156 -
    17.1 --- a/src/Tools/WWW_Find/lighttpd.conf	Sat Apr 26 06:43:06 2014 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,20 +0,0 @@
    17.4 -server.port = 8000
    17.5 -
    17.6 -# debug.log-request-header = "enable"
    17.7 -# debug.log-file-not-found = "enable"
    17.8 -# debug.log-request-handling = "enable"
    17.9 -# debug.log-response-header = "enable"
   17.10 -
   17.11 -mimetype.assign = (
   17.12 -  ".html"   => "text/html; charset=UTF-8",
   17.13 -  ".css"    => "text/css; charset=UTF-8",
   17.14 -)
   17.15 -
   17.16 -server.modules = ( "mod_scgi" )
   17.17 -
   17.18 -scgi.server = ("/isabelle" => ((
   17.19 -		      "host" => "127.0.0.1",
   17.20 -		      "port" => 64000,
   17.21 -		      "check-local" => "disable"
   17.22 -		)))
   17.23 -
    18.1 --- a/src/Tools/WWW_Find/mime.ML	Sat Apr 26 06:43:06 2014 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,56 +0,0 @@
    18.4 -(*  Title:      Tools/WWW_Find/mime.ML
    18.5 -    Author:     Timothy Bourke, NICTA
    18.6 -
    18.7 -Rudimentary support for mime_types.
    18.8 -*)
    18.9 -
   18.10 -signature MIME =
   18.11 -sig
   18.12 -  datatype t = Type of {
   18.13 -      main : string,
   18.14 -      sub : string, 
   18.15 -      params : (string * string) list
   18.16 -    }
   18.17 -
   18.18 -  val plain : t
   18.19 -  val html : t
   18.20 -  
   18.21 -  val parse_type : string -> t option
   18.22 -  val show_type : t -> string
   18.23 -end;
   18.24 -
   18.25 -structure Mime: MIME =
   18.26 -struct
   18.27 -
   18.28 -datatype t = Type of {
   18.29 -    main : string,
   18.30 -    sub : string, 
   18.31 -    params : (string * string) list
   18.32 -  };
   18.33 -
   18.34 -val strip =
   18.35 -  Substring.dropl Char.isSpace
   18.36 -  #> Substring.dropr Char.isSpace;
   18.37 -
   18.38 -val split_fields =
   18.39 -  Substring.splitl (fn c => c <> #"=")
   18.40 -  #> apsnd (Substring.triml 1)
   18.41 -  #> pairself (Substring.string o strip);
   18.42 -
   18.43 -fun show_param (n, v) = implode ["; ", n, "=", v];
   18.44 -
   18.45 -fun show_type (Type {main, sub, params}) =
   18.46 -  implode ([main, "/", sub] @ map show_param params);
   18.47 -
   18.48 -fun parse_type s =
   18.49 -  (case Substring.fields (Char.contains "/;") (Substring.full s) of
   18.50 -     t::s::ps => SOME (Type { main = (Substring.string o strip) t,
   18.51 -                              sub = (Substring.string o strip) s,
   18.52 -                              params = map split_fields ps })
   18.53 -   | _ => NONE);
   18.54 -
   18.55 -val plain = the (parse_type "text/plain; charset=utf-8");
   18.56 -val html = the (parse_type "text/html; charset=utf-8");
   18.57 -
   18.58 -end;
   18.59 -
    19.1 --- a/src/Tools/WWW_Find/scgi_req.ML	Sat Apr 26 06:43:06 2014 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,161 +0,0 @@
    19.4 -(*  Title:      Tools/WWW_Find/scgi_req.ML
    19.5 -    Author:     Timothy Bourke, NICTA
    19.6 -
    19.7 -Parses an SCGI (Simple Common Gateway Interface) header.
    19.8 -See: http://python.ca/scgi/protocol.txt
    19.9 -*)
   19.10 -
   19.11 -signature SCGI_REQ =
   19.12 -sig
   19.13 -  exception InvalidReq of string
   19.14 -
   19.15 -  datatype req_method = Get | Head | Post
   19.16 -
   19.17 -  datatype t = Req of {
   19.18 -      path_info : string,
   19.19 -      path_translated : string,
   19.20 -      script_name : string,
   19.21 -      request_method : req_method,
   19.22 -      query_string : string Symtab.table,
   19.23 -      content_type : Mime.t option,
   19.24 -      environment : Word8VectorSlice.slice Symtab.table
   19.25 -    }
   19.26 -
   19.27 -  val parse : BinIO.instream ->  t * (BinIO.instream * int)
   19.28 -  val test : string -> unit
   19.29 -
   19.30 -  val show : t -> string
   19.31 -end;
   19.32 -
   19.33 -structure ScgiReq : SCGI_REQ =
   19.34 -struct
   19.35 -
   19.36 -exception InvalidReq of string;
   19.37 -
   19.38 -datatype req_method = Get | Head | Post;
   19.39 -
   19.40 -datatype t = Req of {
   19.41 -    path_info : string,
   19.42 -    path_translated : string,
   19.43 -    script_name : string,
   19.44 -    request_method : req_method,
   19.45 -    query_string : string Symtab.table,
   19.46 -    content_type : Mime.t option,
   19.47 -    environment : Word8VectorSlice.slice Symtab.table
   19.48 -  };
   19.49 -
   19.50 -fun parse_req_method "POST" = Post
   19.51 -  | parse_req_method "HEAD" = Head
   19.52 -  | parse_req_method _ = Get;
   19.53 -
   19.54 -fun show_req_method Get = "Get"
   19.55 -  | show_req_method Post = "Post"
   19.56 -  | show_req_method Head = "Head";
   19.57 -
   19.58 -fun find_nulls (idx, 0wx00, idxs) = idx::idxs
   19.59 -  | find_nulls (_, _, idxs) = idxs;
   19.60 -
   19.61 -fun read_net_string fin =
   19.62 -  let
   19.63 -    fun read_size (_, NONE) = raise InvalidReq "Bad netstring length."
   19.64 -      | read_size (t, SOME 0wx3a) = t
   19.65 -      | read_size (t, SOME d) =
   19.66 -          let
   19.67 -            val n = (Word8.toInt d) - 0x30;
   19.68 -          in
   19.69 -            if n >=0 andalso n <= 9
   19.70 -            then read_size (t * 10 + n, BinIO.input1 fin)
   19.71 -            else read_size (t, NONE)
   19.72 -          end;
   19.73 -    val size = read_size (0, BinIO.input1 fin);
   19.74 -    val payload = BinIO.inputN (fin, size);
   19.75 -  in
   19.76 -    (case (Word8Vector.length payload = size, BinIO.input1 fin) of
   19.77 -       (true, SOME 0wx2c) => payload
   19.78 -     | _ => raise InvalidReq "Bad netstring.")
   19.79 -  end;
   19.80 -
   19.81 -fun split_fields vec =
   19.82 -  let
   19.83 -    val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
   19.84 -
   19.85 -    fun pr NONE = "NONE"
   19.86 -      | pr (SOME i) = "SOME " ^ string_of_int i;
   19.87 -
   19.88 -    fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
   19.89 -      | hd_diff _ = NONE;
   19.90 -
   19.91 -    fun slice [] = []
   19.92 -      | slice (idxs as idx::idxs') =
   19.93 -          Word8VectorSlice.slice (vec, idx + 1, hd_diff idxs) :: slice idxs';
   19.94 -
   19.95 -    fun make_pairs (x::y::xys) = (Byte.unpackStringVec x, y) :: make_pairs xys
   19.96 -      | make_pairs _ = [];
   19.97 -
   19.98 -  in make_pairs (slice nulls) end;
   19.99 -
  19.100 -fun parse fin =
  19.101 -  let
  19.102 -    val raw_fields = read_net_string fin;
  19.103 -    val fields = split_fields raw_fields;
  19.104 -    val env = Symtab.make fields;
  19.105 -
  19.106 -    fun field name =
  19.107 -      (case Symtab.lookup env name of
  19.108 -         NONE => ""
  19.109 -       | SOME wv => Byte.unpackStringVec wv);
  19.110 -
  19.111 -    val content_length =
  19.112 -      (case Int.fromString (field "CONTENT_LENGTH") of
  19.113 -        SOME n => n
  19.114 -      | NONE => raise InvalidReq "Bad CONTENT_LENGTH");
  19.115 -
  19.116 -    val req = Req {
  19.117 -        path_info = field "PATH_INFO",
  19.118 -        path_translated = field "PATH_TRANSLATED",
  19.119 -        script_name = field "SCRIPT_NAME",
  19.120 -        request_method = (parse_req_method o field) "REQUEST_METHOD",
  19.121 -        query_string = (HttpUtil.parse_query_string o field) "QUERY_STRING",
  19.122 -        content_type = (Mime.parse_type o field) "CONTENT_TYPE",
  19.123 -        environment = env
  19.124 -      }
  19.125 -
  19.126 -   in (req, (fin, content_length)) end; 
  19.127 -
  19.128 -fun show (Req {path_info, path_translated, script_name,
  19.129 -               request_method, query_string, content_type, environment}) =
  19.130 -  let
  19.131 -    fun show_symtab to_string table = let
  19.132 -        fun show (n, v) r = ["\t", n, " = \"", to_string v, "\"\n"] @ r;
  19.133 -      in Symtab.fold show table [] end;
  19.134 -  in
  19.135 -    implode
  19.136 -      (["path_info: \"", path_info, "\"\n",
  19.137 -        "path_translated: \"", path_translated, "\"\n",
  19.138 -        "script_name: \"", script_name, "\"\n",
  19.139 -        "request_method: \"", show_req_method request_method, "\"\n",
  19.140 -        "query_string:\n"]
  19.141 -       @
  19.142 -       show_symtab I query_string
  19.143 -       @
  19.144 -       ["content_type: ",
  19.145 -          (the_default "" o Option.map Mime.show_type) content_type, "\n",
  19.146 -        "environment:\n"]
  19.147 -       @
  19.148 -       show_symtab Byte.unpackStringVec environment)
  19.149 -  end;
  19.150 -
  19.151 -fun test path =
  19.152 -  let
  19.153 -    val fin = BinIO.openIn path;
  19.154 -    val (req, cs) = parse fin;
  19.155 -    val () = TextIO.print (show req);
  19.156 -    val () =
  19.157 -      BinIO.inputN cs
  19.158 -      |> Word8VectorSlice.full
  19.159 -      |> Byte.unpackStringVec
  19.160 -      |> TextIO.print;
  19.161 -  in BinIO.closeIn fin end;
  19.162 -
  19.163 -end;
  19.164 -
    20.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Sat Apr 26 06:43:06 2014 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,141 +0,0 @@
    20.4 -(*  Title:      Tools/WWW_Find/scgi_server.ML
    20.5 -    Author:     Timothy Bourke, NICTA
    20.6 -
    20.7 -Simple SCGI server.
    20.8 -*)
    20.9 -
   20.10 -signature SCGI_SERVER =
   20.11 -sig
   20.12 -  val max_threads : int Unsynchronized.ref
   20.13 -  type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit
   20.14 -  val register : (string * Mime.t option * handler) -> unit
   20.15 -  val server : string -> int -> unit
   20.16 -  val server' : int -> string -> int -> unit (* keeps trying for port *)
   20.17 -  val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
   20.18 -  val raw_post_handler : (string -> string) -> handler
   20.19 -end;
   20.20 -
   20.21 -structure ScgiServer : SCGI_SERVER =
   20.22 -struct
   20.23 -val max_threads = Unsynchronized.ref 5;
   20.24 -
   20.25 -type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit;
   20.26 -
   20.27 -local
   20.28 -val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table);
   20.29 -in
   20.30 -fun register (name, mime, f) =
   20.31 -  Unsynchronized.change servers (Symtab.update_new (name, (mime, f)));
   20.32 -fun lookup name = Symtab.lookup (!servers) name;
   20.33 -
   20.34 -fun dump_handlers () = (
   20.35 -    tracing("  with handlers:");
   20.36 -    app (fn (x, _) => tracing ("    - " ^ x)) (Symtab.dest (!servers)))
   20.37 -end;
   20.38 -
   20.39 -fun server server_prefix port =
   20.40 -  let
   20.41 -    val passive_sock = Socket_Util.init_server_socket (SOME "localhost") port;
   20.42 -
   20.43 -    val thread_wait = ConditionVar.conditionVar ();
   20.44 -    val thread_wait_mutex = Mutex.mutex ();
   20.45 -
   20.46 -    local
   20.47 -    val threads = Unsynchronized.ref ([] : Thread.thread list);
   20.48 -    fun purge () = Unsynchronized.change threads (filter Thread.isActive);
   20.49 -    in
   20.50 -    fun add_thread th = Unsynchronized.change threads (cons th);
   20.51 -
   20.52 -    fun launch_thread threadf =
   20.53 -      (purge ();
   20.54 -       if length (!threads) < (!max_threads) then ()
   20.55 -       else (tracing ("Waiting for a free thread...");
   20.56 -             ConditionVar.wait (thread_wait, thread_wait_mutex));
   20.57 -       add_thread
   20.58 -         (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
   20.59 -            (fn () => Runtime.exn_trace threadf,
   20.60 -             [Thread.EnableBroadcastInterrupt true,
   20.61 -              Thread.InterruptState
   20.62 -              Thread.InterruptAsynchOnce])))
   20.63 -    end;
   20.64 -
   20.65 -    fun loop () =
   20.66 -      let
   20.67 -        val (sock, _)= Socket.accept passive_sock;
   20.68 -
   20.69 -        val (sin, sout) = Socket_Util.make_streams sock;
   20.70 -
   20.71 -        fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
   20.72 -        fun send_log msg = (tracing msg; send msg);
   20.73 -
   20.74 -        fun get_content (st, 0) = Word8Vector.fromList []
   20.75 -          | get_content x = BinIO.inputN x;
   20.76 -
   20.77 -        fun do_req () =
   20.78 -          let
   20.79 -            val (req as ScgiReq.Req {path_info, request_method, ...},
   20.80 -                 content_is) =
   20.81 -              ScgiReq.parse sin
   20.82 -              handle ScgiReq.InvalidReq s =>
   20.83 -                (send
   20.84 -                   (HttpUtil.reply_header (HttpStatus.bad_request, NONE, []));
   20.85 -                 raise Fail ("Invalid request: " ^ s));
   20.86 -            val () = tracing ("request: " ^ path_info);
   20.87 -          in
   20.88 -            (case lookup (unprefix server_prefix path_info) of
   20.89 -               NONE => send (HttpUtil.reply_header (HttpStatus.not_found, NONE, []))
   20.90 -             | SOME (NONE, f) => f (req, get_content content_is, send)
   20.91 -             | SOME (t, f) =>
   20.92 -                (send (HttpUtil.reply_header (HttpStatus.ok, t, []));
   20.93 -                 if request_method = ScgiReq.Head then ()
   20.94 -                 else f (req, get_content content_is, send)))
   20.95 -          end;
   20.96 -
   20.97 -        fun thread_req () =  (* FIXME avoid handle e *)
   20.98 -          (do_req () handle e => (warning (exnMessage e));
   20.99 -           BinIO.closeOut sout handle e => warning (exnMessage e);
  20.100 -           BinIO.closeIn sin handle e => warning (exnMessage e);
  20.101 -           Socket.close sock handle e => warning (exnMessage e);
  20.102 -           tracing ("request done.");
  20.103 -           ConditionVar.signal thread_wait);
  20.104 -      in
  20.105 -        launch_thread thread_req;
  20.106 -        loop ()
  20.107 -      end;
  20.108 -  in
  20.109 -    tracing ("SCGI server started on port " ^ string_of_int port ^ ".");
  20.110 -    dump_handlers ();
  20.111 -    loop ();
  20.112 -    Socket.close passive_sock
  20.113 -  end;
  20.114 -
  20.115 -local
  20.116 -val delay = 5;
  20.117 -in
  20.118 -fun server' 0 server_prefix port = (warning "Giving up."; exit 1)
  20.119 -  | server' countdown server_prefix port =
  20.120 -      server server_prefix port
  20.121 -        handle OS.SysErr ("bind failed", _) =>
  20.122 -          (warning ("Could not acquire port "
  20.123 -                    ^ string_of_int port ^ ". Trying again in "
  20.124 -                    ^ string_of_int delay ^ " seconds...");
  20.125 -           OS.Process.sleep (Time.fromSeconds delay);
  20.126 -           server' (countdown - 1) server_prefix port);
  20.127 -end;
  20.128 -
  20.129 -fun simple_handler h (ScgiReq.Req {request_method, query_string, ...}, content, send) =
  20.130 -  h (case request_method of
  20.131 -     ScgiReq.Get => query_string
  20.132 -   | ScgiReq.Post =>
  20.133 -      content
  20.134 -      |> Byte.bytesToString
  20.135 -      |> HttpUtil.parse_query_string
  20.136 -   | ScgiReq.Head => raise Fail "Cannot handle Head requests.")
  20.137 -  send;
  20.138 -
  20.139 -fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
  20.140 -      send (h (Byte.bytesToString content))
  20.141 -  | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
  20.142 -
  20.143 -end;
  20.144 -
    21.1 --- a/src/Tools/WWW_Find/socket_util.ML	Sat Apr 26 06:43:06 2014 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,89 +0,0 @@
    21.4 -(*  Title:      Tools/WWW_Find/socket_util.ML
    21.5 -    Author:     Timothy Bourke, NICTA
    21.6 -
    21.7 -Routines for working with sockets.  Following example 10.2 in "The
    21.8 -Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy.
    21.9 -*)
   21.10 -
   21.11 -signature SOCKET_UTIL =
   21.12 -sig
   21.13 -  val init_server_socket: string option -> int -> Socket.passive INetSock.stream_sock
   21.14 -  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
   21.15 -end;
   21.16 -
   21.17 -structure Socket_Util: SOCKET_UTIL =
   21.18 -struct
   21.19 -
   21.20 -fun init_server_socket opt_host port =
   21.21 -  let
   21.22 -    val sock = INetSock.TCP.socket ();
   21.23 -    val addr =
   21.24 -      (case opt_host of
   21.25 -         NONE => INetSock.any port
   21.26 -       | SOME host =>
   21.27 -           NetHostDB.getByName host
   21.28 -           |> the
   21.29 -           |> NetHostDB.addr
   21.30 -           |> rpair port
   21.31 -           |> INetSock.toAddr
   21.32 -           handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host));
   21.33 -    val _ = Socket.bind (sock, addr);
   21.34 -    val _ = Socket.listen (sock, 5);
   21.35 -  in sock end;
   21.36 -
   21.37 -fun make_streams sock =
   21.38 -  let
   21.39 -    val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
   21.40 -
   21.41 -    val sock_name =
   21.42 -      implode [ NetHostDB.toString haddr, ":", string_of_int port ];
   21.43 -
   21.44 -    val rd =
   21.45 -      BinPrimIO.RD {
   21.46 -        name = sock_name,
   21.47 -        chunkSize = Socket.Ctl.getRCVBUF sock,
   21.48 -        readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
   21.49 -        readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
   21.50 -        readVecNB = NONE,
   21.51 -        readArrNB = NONE,
   21.52 -        block = NONE,
   21.53 -        canInput = NONE,
   21.54 -        avail = fn () => NONE,
   21.55 -        getPos = NONE,
   21.56 -        setPos = NONE,
   21.57 -        endPos = NONE,
   21.58 -        verifyPos = NONE,
   21.59 -        close = fn () => Socket.close sock,
   21.60 -        ioDesc = NONE
   21.61 -      };
   21.62 -
   21.63 -    val wr =
   21.64 -      BinPrimIO.WR {
   21.65 -        name = sock_name,
   21.66 -        chunkSize = Socket.Ctl.getSNDBUF sock,
   21.67 -        writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
   21.68 -        writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
   21.69 -        writeVecNB = NONE,
   21.70 -        writeArrNB = NONE,
   21.71 -        block = NONE,
   21.72 -        canOutput = NONE,
   21.73 -        getPos = NONE,
   21.74 -        setPos = NONE,
   21.75 -        endPos = NONE,
   21.76 -        verifyPos = NONE,
   21.77 -        close = fn () => Socket.close sock,
   21.78 -        ioDesc = NONE
   21.79 -      };
   21.80 -
   21.81 -    val in_strm =
   21.82 -      BinIO.mkInstream (
   21.83 -        BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
   21.84 -
   21.85 -    val out_strm =
   21.86 -      BinIO.mkOutstream (
   21.87 -        BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
   21.88 -
   21.89 -    in (in_strm, out_strm) end;
   21.90 -
   21.91 -end;
   21.92 -
    22.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Sat Apr 26 06:43:06 2014 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,279 +0,0 @@
    22.4 -(*  Title:      Tools/WWW_Find/unicode_symbols.ML
    22.5 -    Author:     Timothy Bourke, NICTA
    22.6 -
    22.7 -Parsing of private etc/symbols.
    22.8 -*)
    22.9 -
   22.10 -signature UNICODE_SYMBOLS =
   22.11 -sig
   22.12 -  val symbol_to_unicode : string -> int option
   22.13 -  val abbrev_to_unicode : string -> int option
   22.14 -  val unicode_to_symbol : int -> string option
   22.15 -  val unicode_to_abbrev : int -> string option
   22.16 -  val utf8_to_symbols : string -> string
   22.17 -  val utf8 : int list -> string
   22.18 -end;
   22.19 -
   22.20 -structure UnicodeSymbols : UNICODE_SYMBOLS =
   22.21 -struct
   22.22 -
   22.23 -local (* Lexer *)
   22.24 -
   22.25 -open Basic_Symbol_Pos
   22.26 -
   22.27 -val keywords =
   22.28 -  Scan.make_lexicon (map Symbol.explode ["code", "group", "font", "abbrev", ":"]);
   22.29 -
   22.30 -datatype token_kind =
   22.31 -  Symbol | AsciiSymbol | Keyword | Name | Code | Space | Comment | EOF;
   22.32 -
   22.33 -datatype token = Token of token_kind * string * Position.range;
   22.34 -
   22.35 -fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
   22.36 -
   22.37 -in
   22.38 -
   22.39 -fun mk_eof pos = Token (EOF, "", (pos, Position.none));
   22.40 -
   22.41 -fun str_of_token (Token (_, s, _)) = s;
   22.42 -
   22.43 -fun pos_of_token (Token (_, _, (pos, _))) = pos;
   22.44 -
   22.45 -fun int_of_code (Token (Code, s, _)) = #value (Lexicon.read_xnum s)
   22.46 -  | int_of_code _ = error "internal error in UnicodeSymbols.int_of_code"
   22.47 -
   22.48 -fun is_proper (Token (Space, _, _)) = false
   22.49 -  | is_proper (Token (Comment, _, _)) = false
   22.50 -  | is_proper _ = true;
   22.51 -
   22.52 -fun is_keyword kw (Token (Keyword, kw', _)) = (kw = kw')
   22.53 -  | is_keyword _ _ = false;
   22.54 -
   22.55 -fun is_ascii_sym (Token (AsciiSymbol, _, _)) = true
   22.56 -  | is_ascii_sym _ = false;
   22.57 -
   22.58 -fun is_hex_code (Token (Code, _, _)) = true
   22.59 -  | is_hex_code _ = false;
   22.60 -
   22.61 -fun is_symbol (Token (Symbol, _, _)) = true
   22.62 -  | is_symbol _ = false;
   22.63 -
   22.64 -fun is_name (Token (Name, _, _)) = true
   22.65 -  | is_name _ = false;
   22.66 -
   22.67 -fun is_eof (Token (EOF, _, _)) = true
   22.68 -  | is_eof _ = false;
   22.69 -
   22.70 -fun end_position_of (Token (_, _, (_, epos))) = epos;
   22.71 -
   22.72 -val is_space = Symbol_Pos.symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
   22.73 -val scan_space =
   22.74 -  (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
   22.75 -   ||
   22.76 -   Scan.many is_space @@@ ($$$ "\n")) >> token Space;
   22.77 -
   22.78 -val scan_code = Lexicon.scan_hex #>> token Code;
   22.79 -
   22.80 -val scan_ascii_symbol = Scan.one
   22.81 -  ((fn x => Symbol.is_ascii x andalso
   22.82 -      not (Symbol.is_ascii_letter x
   22.83 -           orelse Symbol.is_ascii_digit x
   22.84 -           orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
   22.85 -  -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
   22.86 -  >> (token AsciiSymbol o op ::);
   22.87 -
   22.88 -fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
   22.89 -val scan_comment =
   22.90 -  $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   22.91 -  >> token Comment;
   22.92 -
   22.93 -fun is_sym s =
   22.94 -  (case Symbol.decode s of
   22.95 -    Symbol.Sym _ => true
   22.96 -  | Symbol.Ctrl _ => true
   22.97 -  | _ => false);
   22.98 -
   22.99 -fun tokenize syms =
  22.100 -  let
  22.101 -    val scanner =
  22.102 -      Scan.one (is_sym o Symbol_Pos.symbol) >> (token Symbol o single) ||
  22.103 -      scan_comment ||
  22.104 -      scan_space ||
  22.105 -      scan_code ||
  22.106 -      Scan.literal keywords >> token Keyword ||
  22.107 -      scan_ascii_symbol ||
  22.108 -      Lexicon.scan_id >> token Name;
  22.109 -    val scan_token = Symbol_Pos.!!! (fn () => "Lexical error") (Scan.bulk scanner);
  22.110 -  in
  22.111 -    (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
  22.112 -      (toks, []) => toks
  22.113 -    | (_, ss) =>
  22.114 -        error ("Lexical error at: " ^ Symbol_Pos.content ss ^
  22.115 -          Position.here (#1 (Symbol_Pos.range ss))))
  22.116 -  end;
  22.117 -
  22.118 -val stopper =
  22.119 -  Scan.stopper
  22.120 -    (fn [] => mk_eof Position.none
  22.121 -      | toks => mk_eof (end_position_of (List.last toks))) is_eof;
  22.122 -
  22.123 -end;
  22.124 -
  22.125 -local (* Parser *)
  22.126 -
  22.127 -fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
  22.128 -val hex_code = Scan.one is_hex_code >> int_of_code;
  22.129 -val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
  22.130 -val symbol = Scan.one is_symbol >> (fn t => (str_of_token t, pos_of_token t));
  22.131 -val name = Scan.one is_name >> str_of_token;
  22.132 -
  22.133 -val unicode = $$$ "code" -- $$$ ":" |-- hex_code;
  22.134 -val group = Scan.option ($$$ "group" -- $$$ ":" |-- name);
  22.135 -val font = Scan.option ($$$ "font" -- $$$ ":" |-- name);
  22.136 -val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
  22.137 -                        |-- (ascii_sym || $$$ ":" || name));
  22.138 -
  22.139 -in
  22.140 -
  22.141 -val line = (symbol -- unicode -- group -- font -- abbr)
  22.142 -  >> (fn ((((a, b), _), _), c) => (a, b, c));
  22.143 -
  22.144 -end;
  22.145 -
  22.146 -local (* build tables *)
  22.147 -
  22.148 -fun add_entries ((fromsym, fromabbr, tosym, toabbr), ((sym, pos), uni, oabbr)) =
  22.149 -  (case oabbr of
  22.150 -     NONE =>
  22.151 -       (Symtab.update_new (sym, uni) fromsym,
  22.152 -        fromabbr,
  22.153 -        Inttab.update (uni, sym) tosym,
  22.154 -        toabbr)
  22.155 -   | SOME abbr =>
  22.156 -       (Symtab.update_new (sym, uni) fromsym,
  22.157 -        Symtab.update_new (abbr, uni) fromabbr,
  22.158 -        Inttab.update (uni, sym) tosym,
  22.159 -        Inttab.update (uni, abbr) toabbr))
  22.160 -  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.here pos)
  22.161 -       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos);
  22.162 -
  22.163 -in
  22.164 -
  22.165 -fun read_symbols path =
  22.166 -  let
  22.167 -    val parsed_lines =
  22.168 -      Symbol_Pos.explode (File.read path, Path.position path)
  22.169 -      |> tokenize
  22.170 -      |> filter is_proper
  22.171 -      |> Scan.finite stopper (Scan.repeat line)
  22.172 -      |> fst;
  22.173 -  in
  22.174 -    Library.foldl add_entries
  22.175 -      ((Symtab.empty, Symtab.empty, Inttab.empty, Inttab.empty),
  22.176 -       parsed_lines)
  22.177 -  end;
  22.178 -
  22.179 -end;
  22.180 -
  22.181 -local
  22.182 -val (fromsym, fromabbr, tosym, toabbr) =
  22.183 -  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
  22.184 -in
  22.185 -val symbol_to_unicode = Symtab.lookup fromsym;
  22.186 -val abbrev_to_unicode = Symtab.lookup fromabbr;
  22.187 -val unicode_to_symbol = Inttab.lookup tosym;
  22.188 -val unicode_to_abbrev = Inttab.lookup toabbr;
  22.189 -end;
  22.190 -
  22.191 -fun utf8_to_symbols utf8str =
  22.192 -  let
  22.193 -    val get_next =
  22.194 -      Substring.getc
  22.195 -      #> Option.map (apfst Byte.charToByte);
  22.196 -    val wstr = String.str o Byte.byteToChar;
  22.197 -    val replacement_char = "\<questiondown>";
  22.198 -
  22.199 -    fun word_to_symbol w =
  22.200 -      (case (unicode_to_symbol o Word32.toInt) w of
  22.201 -         NONE => "?"
  22.202 -       | SOME s => s);
  22.203 -
  22.204 -    fun andb32 (w1, w2) =
  22.205 -      Word8.andb(w1, w2)
  22.206 -      |> Word8.toLarge
  22.207 -      |> Word32.fromLarge;
  22.208 -
  22.209 -    fun read_next (ss, 0, c) = (word_to_symbol c, ss)
  22.210 -      | read_next (ss, n, c) =
  22.211 -          (case get_next ss of
  22.212 -             NONE => (replacement_char, ss)
  22.213 -           | SOME (w, ss') =>
  22.214 -               if Word8.andb (w, 0wxc0) <> 0wx80
  22.215 -               then (replacement_char, ss')
  22.216 -               else
  22.217 -                 let
  22.218 -                   val w' = (Word8.andb (w, 0wx3f));
  22.219 -                   val bw = (Word32.fromLarge o Word8.toLarge) w';
  22.220 -                   val c' = Word32.<< (c, 0wx6);
  22.221 -                 in read_next (ss', n - 1, Word32.orb (c', bw)) end);
  22.222 -
  22.223 -    fun do_char (w, ss) =
  22.224 -      if Word8.andb (w, 0wx80) = 0wx00
  22.225 -      then (wstr w, ss)
  22.226 -      else if Word8.andb (w, 0wx60) = 0wx40
  22.227 -      then read_next (ss, 1, andb32 (w, 0wx1f))
  22.228 -      else if Word8.andb (w, 0wxf0) = 0wxe0
  22.229 -      then read_next (ss, 2, andb32 (w, 0wx0f))
  22.230 -      else if Word8.andb (w, 0wxf8) = 0wxf0
  22.231 -      then read_next (ss, 3, andb32 (w, 0wx07))
  22.232 -      else (replacement_char, ss);
  22.233 -
  22.234 -    fun read (rs, ss) =
  22.235 -      (case Option.map do_char (get_next ss) of
  22.236 -         NONE => (implode o rev) rs
  22.237 -       | SOME (s, ss') => read (s::rs, ss'));
  22.238 -  in read ([], Substring.full utf8str) end;
  22.239 -
  22.240 -local
  22.241 -
  22.242 -fun consec n =
  22.243 -  fn w => (
  22.244 -    Word32.>> (w, Word.fromInt (n * 6))
  22.245 -    |> (curry Word32.andb) 0wx3f
  22.246 -    |> (curry Word32.orb) 0wx80
  22.247 -    |> Word8.fromLargeWord o Word32.toLargeWord);
  22.248 -
  22.249 -fun stamp n =
  22.250 -  fn w => (
  22.251 -    Word32.>> (w, Word.fromInt (n * 6))
  22.252 -    |> (curry Word32.andb) (Word32.>> (0wx000000ff, Word.fromInt (n + 2)))
  22.253 -    |> (curry Word32.orb) (Word32.<< (0wxffffffff, Word.fromInt (7 - n)))
  22.254 -    |> Word8.fromLargeWord o Word32.toLargeWord);
  22.255 -
  22.256 -fun to_utf8_bytes i =
  22.257 -  if i <= 0x007f
  22.258 -  then [Word8.fromInt i]
  22.259 -  else let
  22.260 -    val w = Word32.fromInt i;
  22.261 -  in
  22.262 -    if i < 0x07ff
  22.263 -    then [stamp 1 w, consec 0 w]
  22.264 -    else if i < 0xffff
  22.265 -    then [stamp 2 w, consec 1 w, consec 0 w]
  22.266 -    else if i < 0x10ffff
  22.267 -    then [stamp 3 w, consec 2 w, consec 1 w, consec 0 w]
  22.268 -    else []
  22.269 -  end;
  22.270 -
  22.271 -in
  22.272 -
  22.273 -fun utf8 is =
  22.274 -  map to_utf8_bytes is
  22.275 -  |> flat
  22.276 -  |> Word8Vector.fromList
  22.277 -  |> Byte.bytesToString;
  22.278 -
  22.279 -end
  22.280 -
  22.281 -end;
  22.282 -
    23.1 --- a/src/Tools/WWW_Find/www/basic.css	Sat Apr 26 06:43:06 2014 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,109 +0,0 @@
    23.4 -
    23.5 -body {
    23.6 -    font-family: sans-serif;
    23.7 -    background-color: white;
    23.8 -}
    23.9 -
   23.10 -p.error {
   23.11 -    font-weight: bold;
   23.12 -    color: #ff0000;
   23.13 -}
   23.14 -
   23.15 -p.info {
   23.16 -    font-style: italic;
   23.17 -}
   23.18 -
   23.19 -input#query {
   23.20 -    width: 100%;
   23.21 -}
   23.22 -
   23.23 -legend {
   23.24 -    padding : 0.5em;
   23.25 -    font-weight: bold;
   23.26 -}
   23.27 -
   23.28 -label {
   23.29 -    width: 8em;
   23.30 -    float: left;
   23.31 -}
   23.32 -
   23.33 -fieldset {
   23.34 -    padding: 0 1em 1em 1em;
   23.35 -}
   23.36 -
   23.37 -div.settings {
   23.38 -    padding-top: 2em;
   23.39 -    float: left;
   23.40 -}
   23.41 -
   23.42 -div.settings label {
   23.43 -    font-style: italic;
   23.44 -}
   23.45 -
   23.46 -div.settings div {
   23.47 -    padding-top: 1ex;
   23.48 -}
   23.49 -
   23.50 -div.mainbuttons {
   23.51 -    margin-top: 8.5ex;
   23.52 -    float: right
   23.53 -}
   23.54 -
   23.55 -div.mainbuttons #reset {
   23.56 -    margin-right: 5em;
   23.57 -}
   23.58 -
   23.59 -table.findtheorems {
   23.60 -    width: 100%;
   23.61 -    padding-top: 1em;
   23.62 -    padding-bottom: 2em;
   23.63 -}
   23.64 -
   23.65 -table.findtheorems tr.row0 { background-color: white; }
   23.66 -table.findtheorems tr.row1 { background-color: #f5f5f5; }
   23.67 -table.findtheorems tbody tr:hover { background-color: #dcdcdc; }
   23.68 -
   23.69 -table.findtheorems td {
   23.70 -    vertical-align: top;
   23.71 -    padding-left: 1em;
   23.72 -    padding-bottom: 1em;
   23.73 -}
   23.74 -
   23.75 -table.findtheorems td.name {
   23.76 -    font-size: small;
   23.77 -    font-style: italic;
   23.78 -    padding-right: 1em;
   23.79 -}
   23.80 -table.findtheorems td.thm {
   23.81 -    vertical-align: top;
   23.82 -    font-size: small;
   23.83 -}
   23.84 -table.findtheorems td.thm pre {
   23.85 -    margin: 0em;
   23.86 -}
   23.87 -table.findtheorems th {
   23.88 -    text-align: left;
   23.89 -    padding-bottom: 1ex;
   23.90 -}
   23.91 -
   23.92 -table.findtheoremsquery th {
   23.93 -    font-weight: normal;
   23.94 -    text-align: left;
   23.95 -    padding-top: 1em;
   23.96 -}
   23.97 -
   23.98 -span.class { color: #ff0000 }
   23.99 -span.tfree { color: #9370d8 }
  23.100 -span.tvar { color: #9370d8 }
  23.101 -span.free { color: #add8e6 }
  23.102 -span.bound { color: #008400 }
  23.103 -span.var { color: #00008b }
  23.104 -span.xstr { color: #000000 }
  23.105 -
  23.106 -span.sorried:after { content: " [!]"; }
  23.107 -
  23.108 -div.help a {
  23.109 -    font-size: xx-small;
  23.110 -    color: #d3d3d3;
  23.111 -}
  23.112 -
    24.1 --- a/src/Tools/WWW_Find/www/find_theorems.js	Sat Apr 26 06:43:06 2014 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,406 +0,0 @@
    24.4 -/*
    24.5 - * Author: Timothy Bourke, NICTA
    24.6 - */
    24.7 -var utf8 = new Object();
    24.8 -utf8['\\<supseteq>'] = 'โŠ‡';
    24.9 -utf8['\\<KK>'] = '๐”Ž';
   24.10 -utf8['\\<up>'] = 'โ†‘';
   24.11 -utf8['\\<otimes>'] = 'โŠ—';
   24.12 -utf8['\\<aa>'] = '๐”ž';
   24.13 -utf8['\\<dagger>'] = 'โ€ ';
   24.14 -utf8['\\<frown>'] = 'โŒข';
   24.15 -utf8['\\<guillemotleft>'] = 'ยซ';
   24.16 -utf8['\\<qq>'] = '๐”ฎ';
   24.17 -utf8['\\<X>'] = '๐’ณ';
   24.18 -utf8['\\<triangleright>'] = 'โ–น';
   24.19 -utf8['\\<guillemotright>'] = 'ยป';
   24.20 -utf8['\\<nu>'] = 'ฮฝ';
   24.21 -utf8['\\<sim>'] = 'โˆผ';
   24.22 -utf8['\\<rightharpoondown>'] = 'โ‡';
   24.23 -utf8['\\<p>'] = '๐—‰';
   24.24 -utf8['\\<Up>'] = 'โ‡‘';
   24.25 -utf8['\\<triangleq>'] = 'โ‰œ';
   24.26 -utf8['\\<nine>'] = '๐Ÿต';
   24.27 -utf8['\\<preceq>'] = 'โ‰ผ';
   24.28 -utf8['\\<nabla>'] = 'โˆ‡';
   24.29 -utf8['\\<FF>'] = '๐”‰';
   24.30 -utf8['\\<II>'] = 'โ„‘';
   24.31 -utf8['\\<VV>'] = '๐”™';
   24.32 -utf8['\\<and>'] = 'โˆง';
   24.33 -utf8['\\<mapsto>'] = 'โ†ฆ';
   24.34 -utf8['\\<ll>'] = '๐”ฉ';
   24.35 -utf8['\\<F>'] = 'โ„ฑ';
   24.36 -utf8['\\<degree>'] = 'ยฐ';
   24.37 -utf8['\\<beta>'] = 'ฮฒ';
   24.38 -utf8['\\<Colon>'] = 'โˆท';
   24.39 -utf8['\\<bool>'] = '๐”น';
   24.40 -utf8['\\<e>'] = '๐–พ';
   24.41 -utf8['\\<lozenge>'] = 'โ—Š';
   24.42 -utf8['\\<u>'] = '๐—Ž';
   24.43 -utf8['\\<sharp>'] = 'โ™ฏ';
   24.44 -utf8['\\<Longleftrightarrow>'] = 'โŸบ';
   24.45 -utf8['\\<Otimes>'] = 'โจ‚';
   24.46 -utf8['\\<EE>'] = '๐”ˆ';
   24.47 -utf8['\\<I>'] = 'โ„';
   24.48 -utf8['\\<UU>'] = '๐”˜';
   24.49 -utf8['\\<exclamdown>'] = 'ยก';
   24.50 -utf8['\\<dots>'] = 'โ€ฆ';
   24.51 -utf8['\\<N>'] = '๐’ฉ';
   24.52 -utf8['\\<kk>'] = '๐”จ';
   24.53 -utf8['\\<plusminus>'] = 'ยฑ';
   24.54 -utf8['\\<E>'] = 'โ„ฐ';
   24.55 -utf8['\\<triangle>'] = 'โ–ณ';
   24.56 -utf8['\\<eta>'] = 'ฮท';
   24.57 -utf8['\\<triangleleft>'] = 'โ—ƒ';
   24.58 -utf8['\\<chi>'] = 'ฯ‡';
   24.59 -utf8['\\<z>'] = '๐—“';
   24.60 -utf8['\\<hungarumlaut>'] = 'ห';
   24.61 -utf8['\\<partial>'] = 'โˆ‚';
   24.62 -utf8['\\<three>'] = '๐Ÿฏ';
   24.63 -utf8['\\<lesssim>'] = 'โ‰ฒ';
   24.64 -utf8['\\<subset>'] = 'โŠ‚';
   24.65 -utf8['\\<H>'] = 'โ„‹';
   24.66 -utf8['\\<leftarrow>'] = 'โ†';
   24.67 -utf8['\\<PP>'] = '๐”“';
   24.68 -utf8['\\<sqsupseteq>'] = 'โŠ’';
   24.69 -utf8['\\<R>'] = 'โ„›';
   24.70 -utf8['\\<bowtie>'] = 'โจ';
   24.71 -utf8['\\<C>'] = '๐’ž';
   24.72 -utf8['\\<ddagger>'] = 'โ€ก';
   24.73 -utf8['\\<ff>'] = '๐”ฃ';
   24.74 -utf8['\\<turnstile>'] = 'โŠข';
   24.75 -utf8['\\<bar>'] = 'ยฆ';
   24.76 -utf8['\\<propto>'] = 'โˆ';
   24.77 -utf8['\\<S>'] = '๐’ฎ';
   24.78 -utf8['\\<vv>'] = '๐”ณ';
   24.79 -utf8['\\<lhd>'] = 'โŠฒ';
   24.80 -utf8['\\<paragraph>'] = 'ยถ';
   24.81 -utf8['\\<mu>'] = 'ฮผ';
   24.82 -utf8['\\<rightharpoonup>'] = 'โ‡€';
   24.83 -utf8['\\<Inter>'] = 'โ‹‚';
   24.84 -utf8['\\<o>'] = '๐—ˆ';
   24.85 -utf8['\\<asymp>'] = 'โ‰';
   24.86 -utf8['\\<Leftarrow>'] = 'โ‡';
   24.87 -utf8['\\<Sqinter>'] = 'โจ…';
   24.88 -utf8['\\<eight>'] = '๐Ÿด';
   24.89 -utf8['\\<succeq>'] = 'โ‰ฝ';
   24.90 -utf8['\\<forall>'] = 'โˆ€';
   24.91 -utf8['\\<complex>'] = 'โ„‚';
   24.92 -utf8['\\<GG>'] = '๐”Š';
   24.93 -utf8['\\<Coprod>'] = 'โˆ';
   24.94 -utf8['\\<L>'] = 'โ„’';
   24.95 -utf8['\\<WW>'] = '๐”š';
   24.96 -utf8['\\<leadsto>'] = 'โ†';
   24.97 -utf8['\\<D>'] = '๐’Ÿ';
   24.98 -utf8['\\<angle>'] = 'โˆ ';
   24.99 -utf8['\\<section>'] = 'ยง';
  24.100 -utf8['\\<TTurnstile>'] = 'โŠซ';
  24.101 -utf8['\\<mm>'] = '๐”ช';
  24.102 -utf8['\\<T>'] = '๐’ฏ';
  24.103 -utf8['\\<alpha>'] = 'ฮฑ';
  24.104 -utf8['\\<leftharpoondown>'] = 'โ†ฝ';
  24.105 -utf8['\\<rho>'] = 'ฯ';
  24.106 -utf8['\\<wrong>'] = 'โ‰€';
  24.107 -utf8['\\<l>'] = '๐—…';
  24.108 -utf8['\\<doteq>'] = 'โ‰';
  24.109 -utf8['\\<times>'] = 'ร—';
  24.110 -utf8['\\<noteq>'] = 'โ‰ ';
  24.111 -utf8['\\<rangle>'] = 'โŸฉ';
  24.112 -utf8['\\<div>'] = 'รท';
  24.113 -utf8['\\<Longrightarrow>'] = 'โŸน';
  24.114 -utf8['\\<BB>'] = '๐”…';
  24.115 -utf8['\\<sqsupset>'] = 'โŠ';
  24.116 -utf8['\\<rightarrow>'] = 'โ†’';
  24.117 -utf8['\\<real>'] = 'โ„';
  24.118 -utf8['\\<hh>'] = '๐”ฅ';
  24.119 -utf8['\\<Phi>'] = 'ฮฆ';
  24.120 -utf8['\\<integral>'] = 'โˆซ';
  24.121 -utf8['\\<CC>'] = 'โ„ญ';
  24.122 -utf8['\\<euro>'] = 'โ‚ฌ';
  24.123 -utf8['\\<xx>'] = '๐”ต';
  24.124 -utf8['\\<Y>'] = '๐’ด';
  24.125 -utf8['\\<zeta>'] = 'ฮถ';
  24.126 -utf8['\\<longleftarrow>'] = 'โŸต';
  24.127 -utf8['\\<a>'] = '๐–บ';
  24.128 -utf8['\\<onequarter>'] = 'ยผ';
  24.129 -utf8['\\<And>'] = 'โ‹€';
  24.130 -utf8['\\<downharpoonright>'] = 'โ‡‚';
  24.131 -utf8['\\<phi>'] = 'ฯ†';
  24.132 -utf8['\\<q>'] = '๐—Š';
  24.133 -utf8['\\<Rightarrow>'] = 'โ‡’';
  24.134 -utf8['\\<clubsuit>'] = 'โ™ฃ';
  24.135 -utf8['\\<ggreater>'] = 'โ‰ซ';
  24.136 -utf8['\\<two>'] = '๐Ÿฎ';
  24.137 -utf8['\\<succ>'] = 'โ‰ป';
  24.138 -utf8['\\<AA>'] = '๐”„';
  24.139 -utf8['\\<lparr>'] = 'โฆ‡';
  24.140 -utf8['\\<Squnion>'] = 'โจ†';
  24.141 -utf8['\\<HH>'] = 'โ„Œ';
  24.142 -utf8['\\<sqsubseteq>'] = 'โŠ‘';
  24.143 -utf8['\\<QQ>'] = '๐””';
  24.144 -utf8['\\<setminus>'] = 'โˆ–';
  24.145 -utf8['\\<Lambda>'] = 'ฮ›';
  24.146 -utf8['\\<RR>'] = 'โ„œ';
  24.147 -utf8['\\<J>'] = '๐’ฅ';
  24.148 -utf8['\\<gg>'] = '๐”ค';
  24.149 -utf8['\\<hyphen>'] = 'ยญ';
  24.150 -utf8['\\<B>'] = 'โ„ฌ';
  24.151 -utf8['\\<Z>'] = '๐’ต';
  24.152 -utf8['\\<ww>'] = '๐”ด';
  24.153 -utf8['\\<lambda>'] = 'ฮป';
  24.154 -utf8['\\<onehalf>'] = 'ยฝ';
  24.155 -utf8['\\<f>'] = '๐–ฟ';
  24.156 -utf8['\\<Or>'] = 'โ‹';
  24.157 -utf8['\\<v>'] = '๐—';
  24.158 -utf8['\\<natural>'] = 'โ™ฎ';
  24.159 -utf8['\\<seven>'] = '๐Ÿณ';
  24.160 -utf8['\\<Oplus>'] = 'โจ';
  24.161 -utf8['\\<subseteq>'] = 'โŠ†';
  24.162 -utf8['\\<rfloor>'] = 'โŒ‹';
  24.163 -utf8['\\<LL>'] = '๐”';
  24.164 -utf8['\\<Sum>'] = 'โˆ‘';
  24.165 -utf8['\\<ominus>'] = 'โŠ–';
  24.166 -utf8['\\<bb>'] = '๐”Ÿ';
  24.167 -utf8['\\<Pi>'] = 'ฮ ';
  24.168 -utf8['\\<cent>'] = 'ยข';
  24.169 -utf8['\\<diamond>'] = 'โ—‡';
  24.170 -utf8['\\<mho>'] = 'โ„ง';
  24.171 -utf8['\\<O>'] = '๐’ช';
  24.172 -utf8['\\<rr>'] = '๐”ฏ';
  24.173 -utf8['\\<leftharpoonup>'] = 'โ†ผ';
  24.174 -utf8['\\<pi>'] = 'ฯ€';
  24.175 -utf8['\\<k>'] = '๐—„';
  24.176 -utf8['\\<star>'] = 'โ‹†';
  24.177 -utf8['\\<rightleftharpoons>'] = 'โ‡Œ';
  24.178 -utf8['\\<equiv>'] = 'โ‰ก';
  24.179 -utf8['\\<langle>'] = 'โŸจ';
  24.180 -utf8['\\<Longleftarrow>'] = 'โŸธ';
  24.181 -utf8['\\<nexists>'] = 'โˆ„';
  24.182 -utf8['\\<Odot>'] = 'โจ€';
  24.183 -utf8['\\<lfloor>'] = 'โŒŠ';
  24.184 -utf8['\\<sqsubset>'] = 'โŠ';
  24.185 -utf8['\\<SS>'] = '๐”–';
  24.186 -utf8['\\<box>'] = 'โ–ก';
  24.187 -utf8['\\<index>'] = 'ฤฑ';
  24.188 -utf8['\\<pounds>'] = 'ยฃ';
  24.189 -utf8['\\<Upsilon>'] = 'ฮฅ';
  24.190 -utf8['\\<ii>'] = '๐”ฆ';
  24.191 -utf8['\\<hookleftarrow>'] = 'โ†ฉ';
  24.192 -utf8['\\<P>'] = '๐’ซ';
  24.193 -utf8['\\<epsilon>'] = 'ฮต';
  24.194 -utf8['\\<yy>'] = '๐”ถ';
  24.195 -utf8['\\<h>'] = '๐—';
  24.196 -utf8['\\<upsilon>'] = 'ฯ…';
  24.197 -utf8['\\<x>'] = '๐—‘';
  24.198 -utf8['\\<not>'] = 'ยฌ';
  24.199 -utf8['\\<le>'] = 'โ‰ค';
  24.200 -utf8['\\<one>'] = '๐Ÿญ';
  24.201 -utf8['\\<cdots>'] = 'โ‹ฏ';
  24.202 -utf8['\\<some>'] = 'ฯต';
  24.203 -utf8['\\<Prod>'] = 'โˆ';
  24.204 -utf8['\\<NN>'] = '๐”‘';
  24.205 -utf8['\\<squnion>'] = 'โŠ”';
  24.206 -utf8['\\<dd>'] = '๐”ก';
  24.207 -utf8['\\<top>'] = 'โŠค';
  24.208 -utf8['\\<dieresis>'] = 'ยจ';
  24.209 -utf8['\\<tt>'] = '๐”ฑ';
  24.210 -utf8['\\<U>'] = '๐’ฐ';
  24.211 -utf8['\\<unlhd>'] = 'โŠด';
  24.212 -utf8['\\<cedilla>'] = 'ยธ';
  24.213 -utf8['\\<kappa>'] = 'ฮบ';
  24.214 -utf8['\\<amalg>'] = 'โจฟ';
  24.215 -utf8['\\<restriction>'] = 'โ†พ';
  24.216 -utf8['\\<struct>'] = 'โ‹„';
  24.217 -utf8['\\<m>'] = '๐—†';
  24.218 -utf8['\\<six>'] = '๐Ÿฒ';
  24.219 -utf8['\\<midarrow>'] = 'โ”€';
  24.220 -utf8['\\<lbrace>'] = 'โฆƒ';
  24.221 -utf8['\\<lessapprox>'] = 'โช…';
  24.222 -utf8['\\<MM>'] = '๐”';
  24.223 -utf8['\\<down>'] = 'โ†“';
  24.224 -utf8['\\<oplus>'] = 'โŠ•';
  24.225 -utf8['\\<wp>'] = 'โ„˜';
  24.226 -utf8['\\<surd>'] = 'โˆš';
  24.227 -utf8['\\<cc>'] = '๐” ';
  24.228 -utf8['\\<bottom>'] = 'โŠฅ';
  24.229 -utf8['\\<copyright>'] = 'ยฉ';
  24.230 -utf8['\\<ZZ>'] = 'โ„จ';
  24.231 -utf8['\\<union>'] = 'โˆช';
  24.232 -utf8['\\<V>'] = '๐’ฑ';
  24.233 -utf8['\\<ss>'] = '๐”ฐ';
  24.234 -utf8['\\<unrhd>'] = 'โŠต';
  24.235 -utf8['\\<b>'] = '๐–ป';
  24.236 -utf8['\\<downharpoonleft>'] = 'โ‡ƒ';
  24.237 -utf8['\\<cdot>'] = 'โ‹…';
  24.238 -utf8['\\<r>'] = '๐—‹';
  24.239 -utf8['\\<Midarrow>'] = 'โ•';
  24.240 -utf8['\\<Down>'] = 'โ‡“';
  24.241 -utf8['\\<diamondsuit>'] = 'โ™ข';
  24.242 -utf8['\\<rbrakk>'] = 'โŸง';
  24.243 -utf8['\\<lless>'] = 'โ‰ช';
  24.244 -utf8['\\<longleftrightarrow>'] = 'โŸท';
  24.245 -utf8['\\<prec>'] = 'โ‰บ';
  24.246 -utf8['\\<emptyset>'] = 'โˆ…';
  24.247 -utf8['\\<rparr>'] = 'โฆˆ';
  24.248 -utf8['\\<Delta>'] = 'ฮ”';
  24.249 -utf8['\\<XX>'] = '๐”›';
  24.250 -utf8['\\<parallel>'] = 'โˆฅ';
  24.251 -utf8['\\<K>'] = '๐’ฆ';
  24.252 -utf8['\\<nn>'] = '๐”ซ';
  24.253 -utf8['\\<registered>'] = 'ยฎ';
  24.254 -utf8['\\<M>'] = 'โ„ณ';
  24.255 -utf8['\\<delta>'] = 'ฮด';
  24.256 -utf8['\\<threequarters>'] = 'ยพ';
  24.257 -utf8['\\<g>'] = '๐—€';
  24.258 -utf8['\\<cong>'] = 'โ‰…';
  24.259 -utf8['\\<tau>'] = 'ฯ„';
  24.260 -utf8['\\<w>'] = '๐—';
  24.261 -utf8['\\<ge>'] = 'โ‰ฅ';
  24.262 -utf8['\\<flat>'] = 'โ™ญ';
  24.263 -utf8['\\<zero>'] = '๐Ÿฌ';
  24.264 -utf8['\\<Uplus>'] = 'โจ„';
  24.265 -utf8['\\<longmapsto>'] = 'โŸผ';
  24.266 -utf8['\\<supset>'] = 'โŠƒ';
  24.267 -utf8['\\<in>'] = 'โˆˆ';
  24.268 -utf8['\\<sqinter>'] = 'โŠ“';
  24.269 -utf8['\\<OO>'] = '๐”’';
  24.270 -utf8['\\<updown>'] = 'โ†•';
  24.271 -utf8['\\<circ>'] = 'โˆ˜';
  24.272 -utf8['\\<rat>'] = 'โ„š';
  24.273 -utf8['\\<stileturn>'] = 'โŠฃ';
  24.274 -utf8['\\<ee>'] = '๐”ข';
  24.275 -utf8['\\<Omega>'] = 'ฮฉ';
  24.276 -utf8['\\<or>'] = 'โˆจ';
  24.277 -utf8['\\<inverse>'] = 'ยฏ';
  24.278 -utf8['\\<rhd>'] = 'โŠณ';
  24.279 -utf8['\\<uu>'] = '๐”ฒ';
  24.280 -utf8['\\<iota>'] = 'ฮน';
  24.281 -utf8['\\<d>'] = '๐–ฝ';
  24.282 -utf8['\\<questiondown>'] = 'ยฟ';
  24.283 -utf8['\\<Union>'] = 'โ‹ƒ';
  24.284 -utf8['\\<omega>'] = 'ฯ‰';
  24.285 -utf8['\\<approx>'] = 'โ‰ˆ';
  24.286 -utf8['\\<t>'] = '๐—';
  24.287 -utf8['\\<Updown>'] = 'โ‡•';
  24.288 -utf8['\\<spadesuit>'] = 'โ™ ';
  24.289 -utf8['\\<five>'] = '๐Ÿฑ';
  24.290 -utf8['\\<exists>'] = 'โˆƒ';
  24.291 -utf8['\\<rceil>'] = 'โŒ‰';
  24.292 -utf8['\\<JJ>'] = '๐”';
  24.293 -utf8['\\<minusplus>'] = 'โˆ“';
  24.294 -utf8['\\<nat>'] = 'โ„•';
  24.295 -utf8['\\<oslash>'] = 'โŠ˜';
  24.296 -utf8['\\<A>'] = '๐’œ';
  24.297 -utf8['\\<Xi>'] = 'ฮž';
  24.298 -utf8['\\<currency>'] = 'ยค';
  24.299 -utf8['\\<Turnstile>'] = 'โŠจ';
  24.300 -utf8['\\<hookrightarrow>'] = 'โ†ช';
  24.301 -utf8['\\<pp>'] = '๐”ญ';
  24.302 -utf8['\\<Q>'] = '๐’ฌ';
  24.303 -utf8['\\<aleph>'] = 'โ„ต';
  24.304 -utf8['\\<acute>'] = 'ยด';
  24.305 -utf8['\\<xi>'] = 'ฮพ';
  24.306 -utf8['\\<simeq>'] = 'โ‰ƒ';
  24.307 -utf8['\\<i>'] = '๐—‚';
  24.308 -utf8['\\<Join>'] = 'โ‹ˆ';
  24.309 -utf8['\\<y>'] = '๐—’';
  24.310 -utf8['\\<lbrakk>'] = 'โŸฆ';
  24.311 -utf8['\\<greatersim>'] = 'โ‰ณ';
  24.312 -utf8['\\<greaterapprox>'] = 'โช†';
  24.313 -utf8['\\<longrightarrow>'] = 'โŸถ';
  24.314 -utf8['\\<lceil>'] = 'โŒˆ';
  24.315 -utf8['\\<Gamma>'] = 'ฮ“';
  24.316 -utf8['\\<odot>'] = 'โŠ™';
  24.317 -utf8['\\<YY>'] = '๐”œ';
  24.318 -utf8['\\<infinity>'] = 'โˆž';
  24.319 -utf8['\\<Sigma>'] = 'ฮฃ';
  24.320 -utf8['\\<yen>'] = 'ยฅ';
  24.321 -utf8['\\<int>'] = 'โ„ค';
  24.322 -utf8['\\<tturnstile>'] = 'โŠฉ';
  24.323 -utf8['\\<oo>'] = '๐”ฌ';
  24.324 -utf8['\\<ointegral>'] = 'โˆฎ';
  24.325 -utf8['\\<gamma>'] = 'ฮณ';
  24.326 -utf8['\\<upharpoonleft>'] = 'โ†ฟ';
  24.327 -utf8['\\<sigma>'] = 'ฯƒ';
  24.328 -utf8['\\<n>'] = '๐—‡';
  24.329 -utf8['\\<rbrace>'] = 'โฆ„';
  24.330 -utf8['\\<DD>'] = '๐”‡';
  24.331 -utf8['\\<notin>'] = 'โˆ‰';
  24.332 -utf8['\\<j>'] = '๐—ƒ';
  24.333 -utf8['\\<uplus>'] = 'โŠŽ';
  24.334 -utf8['\\<leftrightarrow>'] = 'โ†”';
  24.335 -utf8['\\<TT>'] = '๐”—';
  24.336 -utf8['\\<bullet>'] = 'โˆ™';
  24.337 -utf8['\\<Theta>'] = 'ฮ˜';
  24.338 -utf8['\\<smile>'] = 'โŒฃ';
  24.339 -utf8['\\<G>'] = '๐’ข';
  24.340 -utf8['\\<jj>'] = '๐”ง';
  24.341 -utf8['\\<inter>'] = 'โˆฉ';
  24.342 -utf8['\\<Psi>'] = 'ฮจ';
  24.343 -utf8['\\<ordfeminine>'] = 'ยช';
  24.344 -utf8['\\<W>'] = '๐’ฒ';
  24.345 -utf8['\\<zz>'] = '๐”ท';
  24.346 -utf8['\\<theta>'] = 'ฮธ';
  24.347 -utf8['\\<ordmasculine>'] = 'ยบ';
  24.348 -utf8['\\<c>'] = '๐–ผ';
  24.349 -utf8['\\<psi>'] = 'ฯˆ';
  24.350 -utf8['\\<s>'] = '๐—Œ';
  24.351 -utf8['\\<Leftrightarrow>'] = 'โ‡”';
  24.352 -utf8['\\<heartsuit>'] = 'โ™ก';
  24.353 -utf8['\\<four>'] = '๐Ÿฐ';
  24.354 -
  24.355 -var re_xsymbol = /\\<.*?>/g;
  24.356 -
  24.357 -function encodequery(ele) {
  24.358 -  var text = ele.value;
  24.359 -  var otext = text;
  24.360 -  var pos = getCaret(ele);
  24.361 -
  24.362 -  xsymbols = text.match(re_xsymbol);
  24.363 -  for (i in xsymbols) {
  24.364 -    var repl = utf8[xsymbols[i]];
  24.365 -    if (repl) {
  24.366 -	text = text.replace(xsymbols[i], repl, "g");
  24.367 -    }
  24.368 -  }
  24.369 -
  24.370 -  if (text != otext) {
  24.371 -    ele.value = text;
  24.372 -
  24.373 -    if (pos != -1) {
  24.374 -      pos = pos - (otext.length - text.length);
  24.375 -      setCaret(ele, pos);
  24.376 -    }
  24.377 -  }
  24.378 -}
  24.379 -
  24.380 -/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */
  24.381 -function getCaret(obj) {
  24.382 -  var pos = -1;
  24.383 -
  24.384 -  if (document.selection) { // IE
  24.385 -    obj.focus ();
  24.386 -    var sel = document.selection.createRange();
  24.387 -    var sellen = document.selection.createRange().text.length;
  24.388 -    sel.moveStart ('character', -obj.value.length);
  24.389 -    pos = sel.text.length - sellen;
  24.390 -
  24.391 -  } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko
  24.392 -    pos = obj.selectionStart;
  24.393 -  }
  24.394 -  
  24.395 -  return pos;
  24.396 -}
  24.397 -
  24.398 -/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */
  24.399 -function setCaret(obj, pos) {
  24.400 -  if (obj.createTextRange) {
  24.401 -      var range = obj.createTextRange();
  24.402 -      range.move("character", pos);
  24.403 -      range.select();
  24.404 -  } else if (obj.selectionStart) {
  24.405 -      obj.focus();
  24.406 -      obj.setSelectionRange(pos, pos);
  24.407 -  }
  24.408 -}
  24.409 -
    25.1 --- a/src/Tools/WWW_Find/www/pasting_help.html	Sat Apr 26 06:43:06 2014 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,19 +0,0 @@
    25.4 -<html>
    25.5 -  <head>
    25.6 -    <title>Find Theorems: help pasting from ProofGeneral</title>
    25.7 -    <link rel="stylesheet" type="text/css" href="/basic.css"/>
    25.8 -  </head>
    25.9 -  <body>
   25.10 -    <h1>Pasting theory text from Proof General with x-symbol</h1>
   25.11 -    <ol>
   25.12 -      <li>Select the text using the keyboard (<code>C-SPC</code>, 
   25.13 -      <code>arrow keys</code>).</li>
   25.14 -      <li>Choose <code>X-Symbol</code>/<code>Other 
   25.15 -        Commands</code>/<code>Copy Encoded</code>.</li>
   25.16 -      <li>Paste into the web browser (<code>C-v</code>).</li>
   25.17 -    </ol>
   25.18 -
   25.19 -    <a href="/isabelle/find_theorems">Return to find_theorems</a>
   25.20 -  </body>
   25.21 -</html>
   25.22 -
    26.1 --- a/src/Tools/WWW_Find/xhtml.ML	Sat Apr 26 06:43:06 2014 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,441 +0,0 @@
    26.4 -(*  Title:      Tools/WWW_Find/xhtml.ML
    26.5 -    Author:     Timothy Bourke, NICTA
    26.6 -
    26.7 -Rudimentary XHTML construction.
    26.8 -*)
    26.9 -
   26.10 -signature XHTML =
   26.11 -sig
   26.12 -  type attribute
   26.13 -  type common_atts = { id : string option,
   26.14 -                       class : string option };
   26.15 -  val noid : common_atts;
   26.16 -  val id : string -> common_atts;
   26.17 -  val class : string -> common_atts;
   26.18 -
   26.19 -  type tag
   26.20 -
   26.21 -  val doctype_xhtml1_0_strict: string;
   26.22 -
   26.23 -  val att: string -> string -> attribute
   26.24 -  val bool_att: string * bool -> attribute list
   26.25 -
   26.26 -  val tag: string -> attribute list -> tag list -> tag
   26.27 -  val tag': string -> common_atts -> tag list -> tag
   26.28 -  val text: string -> tag
   26.29 -  val raw_text: string -> tag
   26.30 -
   26.31 -  val add_attributes: attribute list -> tag -> tag
   26.32 -  val append: tag -> tag list -> tag
   26.33 -
   26.34 -  val show: tag -> string list
   26.35 -
   26.36 -  val write: (string -> unit) -> tag -> unit
   26.37 -  val write_enclosed: (string -> unit) -> tag -> ((string -> unit) -> unit) -> unit
   26.38 -
   26.39 -  val html: { lang : string } -> tag list -> tag
   26.40 -  val head: { title : string, stylesheet_href : string } -> tag list -> tag
   26.41 -  val body: common_atts -> tag list -> tag
   26.42 -  val divele: common_atts -> tag list -> tag
   26.43 -  val span: common_atts * string -> tag
   26.44 -  val span': common_atts -> tag list -> tag
   26.45 -
   26.46 -  val pre: common_atts -> string -> tag
   26.47 -
   26.48 -  val table: common_atts -> tag list -> tag
   26.49 -  val thead: common_atts -> tag list -> tag
   26.50 -  val tbody: common_atts -> tag list -> tag
   26.51 -  val tr: tag list -> tag
   26.52 -  val th: common_atts * string -> tag
   26.53 -  val th': common_atts -> tag list -> tag
   26.54 -  val td: common_atts * string -> tag
   26.55 -  val td': common_atts -> tag list -> tag
   26.56 -  val td'': common_atts * { colspan : int option, rowspan : int option }
   26.57 -           -> tag list -> tag
   26.58 -
   26.59 -  val p: common_atts * string -> tag
   26.60 -  val p': common_atts * tag list -> tag
   26.61 -  val h: common_atts * int * string -> tag
   26.62 -  val strong: string -> tag
   26.63 -  val em: string -> tag
   26.64 -  val a: { href : string, text : string } -> tag
   26.65 -
   26.66 -  val ul: common_atts * tag list -> tag
   26.67 -  val ol: common_atts * tag list -> tag
   26.68 -  val dl: common_atts * (string * tag) list -> tag
   26.69 -
   26.70 -  val alternate_class: { class0 : string, class1 : string }
   26.71 -                      -> tag list -> tag list
   26.72 -
   26.73 -  val form: common_atts * { method : string, action : string }
   26.74 -            -> tag list -> tag
   26.75 -
   26.76 -  datatype input_type =
   26.77 -      TextInput of { value: string option, maxlength: int option }
   26.78 -    | Password of int option
   26.79 -    | Checkbox of { checked : bool, value : string option }
   26.80 -    | Radio of { checked : bool, value : string option }
   26.81 -    | Submit
   26.82 -    | Reset
   26.83 -    | Hidden
   26.84 -    | Image of { src : string, alt : string }
   26.85 -    | File of { accept : string }
   26.86 -    | Button;
   26.87 -
   26.88 -  val input: common_atts * { name : string, itype : input_type } -> tag
   26.89 -  val select: common_atts * { name : string, value : string option }
   26.90 -              -> string list -> tag
   26.91 -  val label: common_atts * { for: string } * string -> tag
   26.92 -
   26.93 -  val reset_button: common_atts -> tag
   26.94 -  val submit_button: common_atts -> tag
   26.95 -
   26.96 -  datatype event =
   26.97 -    (* global *)
   26.98 -      OnClick
   26.99 -    | OnDblClick
  26.100 -    | OnMouseDown
  26.101 -    | OnMouseUp
  26.102 -    | OnMouseOver
  26.103 -    | OnMouseMove
  26.104 -    | OnMouseOut
  26.105 -    | OnKeyPress
  26.106 -    | OnKeyDown
  26.107 -    | OnKeyUp
  26.108 -      (* anchor/label/input/select/textarea/button/area *)
  26.109 -    | OnFocus
  26.110 -    | OnBlur
  26.111 -      (* form *)
  26.112 -    | OnSubmit
  26.113 -    | OnReset
  26.114 -      (* input/textarea *)
  26.115 -    | OnSelect
  26.116 -      (* input/select/textarea *)
  26.117 -    | OnChange
  26.118 -      (* body *)
  26.119 -    | OnLoad
  26.120 -    | OnUnload;
  26.121 -
  26.122 -  val script: common_atts * { script_type: string, src: string } -> tag
  26.123 -  val add_script: event * string -> tag -> tag
  26.124 -end;
  26.125 -
  26.126 -structure Xhtml : XHTML =
  26.127 -struct
  26.128 -
  26.129 -type attribute = string * string;
  26.130 -type common_atts = {
  26.131 -    id : string option,
  26.132 -    class : string option
  26.133 -  };
  26.134 -val noid = { id = NONE, class = NONE };
  26.135 -fun id s = { id = SOME s, class = NONE };
  26.136 -fun class s = { id = NONE, class = SOME s };
  26.137 -
  26.138 -fun from_common { id = NONE,   class = NONE } = []
  26.139 -  | from_common { id = SOME i, class = NONE } = [("id", i)]
  26.140 -  | from_common { id = NONE,   class = SOME c } = [("class", c)]
  26.141 -  | from_common { id = SOME i, class = SOME c } = [("id", i), ("class", c)];
  26.142 -
  26.143 -val update_atts =
  26.144 -  AList.join (op = : string * string -> bool) (fn _ => snd);
  26.145 -
  26.146 -datatype tag = Tag of (string * attribute list * tag list)
  26.147 -             | Text of string
  26.148 -             | RawText of string;
  26.149 -
  26.150 -fun is_text (Tag _) = false
  26.151 -  | is_text (Text _) = true
  26.152 -  | is_text (RawText _) = true;
  26.153 -
  26.154 -fun is_tag (Tag _) = true
  26.155 -  | is_tag (Text _) = false
  26.156 -  | is_tag (RawText _) = false;
  26.157 -
  26.158 -val att = pair;
  26.159 -
  26.160 -fun bool_att (nm, true) = [(nm, nm)]
  26.161 -  | bool_att (nm, false) = [];
  26.162 -
  26.163 -fun tag name atts inner = Tag (name, atts, inner);
  26.164 -fun tag' name common_atts inner = Tag (name, from_common common_atts, inner);
  26.165 -fun text t = Text t;
  26.166 -fun raw_text t = RawText t;
  26.167 -
  26.168 -fun add_attributes atts' (Tag (nm, atts, inner)) =
  26.169 -      Tag (nm, update_atts (atts, atts'), inner)
  26.170 -  | add_attributes _ t = t;
  26.171 -
  26.172 -fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
  26.173 -  | append _ _ = raise Fail "cannot append to a text element";
  26.174 -
  26.175 -fun show_att (n, v) = implode [" ", n, "=\"", XML.text v, "\""];
  26.176 -
  26.177 -fun show_text (Text t) = XML.text t
  26.178 -  | show_text (RawText t) = t
  26.179 -  | show_text _ = raise Fail "Bad call to show_text.";
  26.180 -
  26.181 -fun show (Text t) = [XML.text t]
  26.182 -  | show (RawText t) = [t]
  26.183 -  | show (Tag (nm, atts, inner)) =
  26.184 -  (["<", nm] @ map show_att atts
  26.185 -   @
  26.186 -   (if length inner = 0
  26.187 -    then ["/>"]
  26.188 -    else flat (
  26.189 -      [[">"]]
  26.190 -      @
  26.191 -      map show inner
  26.192 -      @
  26.193 -      [["</", nm, ">"]]
  26.194 -  )));
  26.195 -
  26.196 -fun write pr =
  26.197 -  let
  26.198 -    fun f (Text t) = (pr o XML.text) t
  26.199 -      | f (RawText t) = pr t
  26.200 -      | f (Tag (nm, atts, inner)) = (
  26.201 -          pr "<";
  26.202 -          pr nm;
  26.203 -          app (pr o show_att) atts;
  26.204 -          if length inner = 0
  26.205 -          then pr "/>"
  26.206 -          else (
  26.207 -            pr ">";
  26.208 -            app f inner;
  26.209 -            pr ("</" ^ nm ^ ">")
  26.210 -          ))
  26.211 -  in f end;
  26.212 -
  26.213 -(* Print all opening tags down into the tree until a branch of degree > 1 is
  26.214 -   found, in which case print everything before the last tag, which is then
  26.215 -   opened. *)
  26.216 -fun write_open pr =
  26.217 -  let
  26.218 -    fun f (Text t) = (pr o XML.text) t
  26.219 -      | f (RawText t) = pr t
  26.220 -      | f (Tag (nm, atts, [])) =
  26.221 -          (pr "<"; pr nm; app (pr o show_att) atts; pr ">")
  26.222 -      | f (Tag (nm, atts, xs)) =
  26.223 -           (pr "<"; pr nm; app (pr o show_att) atts; pr ">";
  26.224 -            (case take_suffix is_text xs of
  26.225 -               ([], _) => ()
  26.226 -             | (b, _) =>
  26.227 -                 let val (xs, x) = split_last b;
  26.228 -                 in app (write pr) xs; f x end));
  26.229 -  in f end;
  26.230 -
  26.231 -(* Print matching closing tags for write_open. *)
  26.232 -fun write_close pr =
  26.233 -  let
  26.234 -    fun close nm = pr ("</" ^ nm ^ ">");
  26.235 -    val pr_text = app (pr o show_text);
  26.236 -
  26.237 -    fun f (Text t) = ()
  26.238 -      | f (RawText t) = ()
  26.239 -      | f (Tag (nm, _, [])) = close nm
  26.240 -      | f (Tag (nm, _, xs)) =
  26.241 -           (case take_suffix is_text xs of
  26.242 -              ([], text) => pr_text text
  26.243 -            | (b, text) =>
  26.244 -                let val (xs, x) = split_last b;
  26.245 -                in f x; close nm; pr_text text end);
  26.246 -  in f end;
  26.247 -
  26.248 -fun write_enclosed pr template content =
  26.249 -  (write_open pr template; content pr; write_close pr template)
  26.250 -
  26.251 -fun html { lang } tags = Tag ("html",
  26.252 -                              [("xmlns", "http://www.w3.org/1999/xhtml"),
  26.253 -                               ("xml:lang", lang)],
  26.254 -                              tags);
  26.255 -
  26.256 -fun head { title, stylesheet_href } inner = let
  26.257 -    val link =
  26.258 -      Tag ("link",
  26.259 -        [("rel", "stylesheet"),
  26.260 -         ("type", "text/css"),
  26.261 -         ("href", stylesheet_href)], []);
  26.262 -    val title = Tag ("title", [], [Text title]);
  26.263 -    val charset = Tag ("meta",
  26.264 -        [("http-equiv", "Content-type"),
  26.265 -         ("content", "text/html; charset=UTF-8")], []);
  26.266 -  in Tag ("head", [], link::title::charset::inner) end;
  26.267 -
  26.268 -fun body common_atts tags = Tag ("body", from_common common_atts, tags);
  26.269 -
  26.270 -fun divele common_atts tags = Tag ("div", from_common common_atts, tags);
  26.271 -fun span (common_atts, t) = Tag ("span", from_common common_atts, [Text t]);
  26.272 -fun span' common_atts tags = Tag ("span", from_common common_atts, tags);
  26.273 -
  26.274 -fun pre common_atts rt = Tag ("pre", from_common common_atts, [RawText rt]);
  26.275 -
  26.276 -fun ostr_att (nm, NONE) = []
  26.277 -  | ostr_att (nm, SOME s) = [(nm, s)];
  26.278 -val oint_att = ostr_att o apsnd (Option.map string_of_int);
  26.279 -
  26.280 -val table = tag' "table";
  26.281 -val thead = tag' "thead";
  26.282 -val tbody = tag' "tbody";
  26.283 -val tr = tag "tr" [];
  26.284 -fun th (common_atts, t) = Tag ("th", from_common common_atts, [Text t]);
  26.285 -fun th' common_atts tags = Tag ("th", from_common common_atts, tags);
  26.286 -fun td (common_atts, t) = Tag ("td", from_common common_atts, [Text t]);
  26.287 -fun td' common_atts tags = Tag ("td", from_common common_atts, tags);
  26.288 -fun td'' (common_atts, { colspan, rowspan }) tags =
  26.289 -  Tag ("td",
  26.290 -    from_common common_atts
  26.291 -    @ oint_att ("colspan", colspan)
  26.292 -    @ oint_att ("rowspan", rowspan),
  26.293 -    tags);
  26.294 -
  26.295 -fun p (common_atts, t) = Tag ("p", from_common common_atts, [Text t]);
  26.296 -fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags);
  26.297 -
  26.298 -fun h (common_atts, i, text) =
  26.299 -  Tag ("h" ^ string_of_int i, from_common common_atts, [Text text]);
  26.300 -
  26.301 -fun strong t = Tag ("strong", [], [Text t]);
  26.302 -fun em t = Tag ("em", [], [Text t]);
  26.303 -fun a { href, text } = Tag ("a", [("href", href)], [Text text]);
  26.304 -
  26.305 -fun to_li tag = Tag ("li", [], [tag]);
  26.306 -fun ul (common_atts, lis) = Tag ("ul", from_common common_atts, map to_li lis);
  26.307 -fun ol (common_atts, lis) = Tag ("ol", from_common common_atts, map to_li lis);
  26.308 -
  26.309 -fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
  26.310 -                         Tag ("dd", [], [tag])];
  26.311 -fun dl (common_atts, dtdds) =
  26.312 -  Tag ("dl", from_common common_atts, maps to_dtdd dtdds);
  26.313 -            
  26.314 -fun alternate_class { class0, class1 } rows = let
  26.315 -    fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)
  26.316 -      | f ((false, xs), x) = (true, add_attributes [("class", class1)] x :: xs);
  26.317 -  in Library.foldl f ((true, []), rows) |> snd |> rev end;
  26.318 -
  26.319 -fun form (common_atts as { id, ... }, { method, action }) tags =
  26.320 -  Tag ("form",
  26.321 -    [("method", method),
  26.322 -     ("action", action)]
  26.323 -    @ from_common common_atts, tags);
  26.324 -
  26.325 -datatype input_type =
  26.326 -    TextInput of { value: string option, maxlength: int option }
  26.327 -  | Password of int option
  26.328 -  | Checkbox of { checked : bool, value : string option }
  26.329 -  | Radio of { checked : bool, value : string option }
  26.330 -  | Submit
  26.331 -  | Reset
  26.332 -  | Hidden
  26.333 -  | Image of { src : string, alt : string }
  26.334 -  | File of { accept : string }
  26.335 -  | Button;
  26.336 -
  26.337 -fun from_checked { checked = false, value = NONE }   = []
  26.338 -  | from_checked { checked = true,  value = NONE }   = [("checked", "checked")]
  26.339 -  | from_checked { checked = false, value = SOME v } = [("value", v)]
  26.340 -  | from_checked { checked = true,  value = SOME v } =
  26.341 -      [("checked", "checked"), ("value", v)];
  26.342 -
  26.343 -fun input_atts (TextInput { value, maxlength }) =
  26.344 -      ("type", "text")
  26.345 -       :: ostr_att ("value", value)
  26.346 -        @ oint_att ("maxlength", maxlength)
  26.347 -  | input_atts (Password NONE) = [("type", "password")]
  26.348 -  | input_atts (Password (SOME i)) =
  26.349 -      [("type", "password"), ("maxlength", string_of_int i)]
  26.350 -  | input_atts (Checkbox checked) =
  26.351 -      ("type", "checkbox") :: from_checked checked
  26.352 -  | input_atts (Radio checked) = ("type", "radio") :: from_checked checked
  26.353 -  | input_atts Submit = [("type", "submit")]
  26.354 -  | input_atts Reset = [("type", "reset")]
  26.355 -  | input_atts Hidden = [("type", "hidden")]
  26.356 -  | input_atts (Image { src, alt }) =
  26.357 -      [("type", "image"), ("src", src), ("alt", alt)]
  26.358 -  | input_atts (File { accept }) = [("type", "file"), ("accept", accept)]
  26.359 -  | input_atts Button = [("type", "button")];
  26.360 -
  26.361 -fun input (common_atts, { name, itype }) =
  26.362 -  Tag ("input",
  26.363 -       input_atts itype @ [("name", name)] @ from_common common_atts,
  26.364 -       []);
  26.365 -
  26.366 -fun reset_button common_atts =
  26.367 -  Tag ("input", input_atts Reset @ from_common common_atts, []);
  26.368 -
  26.369 -fun submit_button common_atts =
  26.370 -  Tag ("input", input_atts Submit @ from_common common_atts, []);
  26.371 -
  26.372 -
  26.373 -fun select (common_atts, { name, value }) options =
  26.374 -  let
  26.375 -    fun is_selected t =
  26.376 -      (case value of
  26.377 -         NONE => []
  26.378 -       | SOME s => if t = s then bool_att ("selected", true) else []);
  26.379 -    fun to_option t = Tag ("option", is_selected t, [Text t]);
  26.380 -  in
  26.381 -    Tag ("select",
  26.382 -      ("name", name) :: from_common common_atts,
  26.383 -      map to_option options)
  26.384 -  end;
  26.385 -
  26.386 -fun label (common_atts, { for }, text) =
  26.387 -  Tag ("label", ("for", for) :: from_common common_atts, [Text text]);
  26.388 -
  26.389 -datatype event =
  26.390 -    OnClick
  26.391 -  | OnDblClick
  26.392 -  | OnMouseDown
  26.393 -  | OnMouseUp
  26.394 -  | OnMouseOver
  26.395 -  | OnMouseMove
  26.396 -  | OnMouseOut
  26.397 -  | OnKeyPress
  26.398 -  | OnKeyDown
  26.399 -  | OnKeyUp
  26.400 -  | OnFocus
  26.401 -  | OnBlur
  26.402 -  | OnSubmit
  26.403 -  | OnReset
  26.404 -  | OnSelect
  26.405 -  | OnChange
  26.406 -  | OnLoad
  26.407 -  | OnUnload;
  26.408 -
  26.409 -fun event_to_str OnClick = "onclick"
  26.410 -  | event_to_str OnDblClick = "ondblclick"
  26.411 -  | event_to_str OnMouseDown = "onmousedown"
  26.412 -  | event_to_str OnMouseUp = "onmouseup"
  26.413 -  | event_to_str OnMouseOver = "onmouseover"
  26.414 -  | event_to_str OnMouseMove = "onmousemove"
  26.415 -  | event_to_str OnMouseOut = "onmouseout"
  26.416 -  | event_to_str OnKeyPress = "onkeypress"
  26.417 -  | event_to_str OnKeyDown = "onkeydown"
  26.418 -  | event_to_str OnKeyUp = "onkeyup"
  26.419 -  | event_to_str OnFocus = "onfocus"
  26.420 -  | event_to_str OnBlur = "onblur"
  26.421 -  | event_to_str OnSubmit = "onsubmit"
  26.422 -  | event_to_str OnReset = "onreset"
  26.423 -  | event_to_str OnSelect = "onselect"
  26.424 -  | event_to_str OnChange = "onchange"
  26.425 -  | event_to_str OnLoad = "onload"
  26.426 -  | event_to_str OnUnload = "onunload";
  26.427 -
  26.428 -fun script (common_atts, {script_type, src}) =
  26.429 -  Tag ("script",
  26.430 -    ("type", script_type)
  26.431 -    :: ("src", src)
  26.432 -    :: from_common common_atts, [text ""]);
  26.433 -
  26.434 -fun add_script (evty, script) (Tag (name, atts, inner))
  26.435 -      = Tag (name, AList.update (op =) (event_to_str evty, script) atts, inner)
  26.436 -  | add_script _ t = t;
  26.437 -
  26.438 -
  26.439 -val doctype_xhtml1_0_strict =
  26.440 -  "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
  26.441 -  \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
  26.442 -
  26.443 -end;
  26.444 -