WWW_Find component: find_theorems via web browser
authorkleing
Fri Nov 20 18:36:44 2009 +1100 (2009-11-20)
changeset 33817f6a4da31f2f1
parent 33816 e08c9f755fca
child 33818 aa00c583f594
WWW_Find component: find_theorems via web browser
etc/components
src/Tools/WWW_Find/IsaMakefile
src/Tools/WWW_Find/ROOT.ML
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/find_theorems.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/etc/components	Fri Nov 20 10:40:30 2009 +0100
     1.2 +++ b/etc/components	Fri Nov 20 18:36:44 2009 +1100
     1.3 @@ -12,6 +12,7 @@
     1.4  src/Sequents
     1.5  #misc components
     1.6  src/Tools/Code
     1.7 +src/Tools/WWW_Find
     1.8  src/HOL/Tools/ATP_Manager
     1.9  src/HOL/Mirabelle
    1.10  src/HOL/Library/Sum_Of_Squares
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/WWW_Find/IsaMakefile	Fri Nov 20 18:36:44 2009 +1100
     2.3 @@ -0,0 +1,21 @@
     2.4 +#
     2.5 +# IsaMakefile for WWW_Find
     2.6 +#
     2.7 +# Provides static compile check for ML files only.
     2.8 +
     2.9 +
    2.10 +OUT = $(ISABELLE_OUTPUT)
    2.11 +LOG = $(OUT)/log
    2.12 +
    2.13 +LOGFILE = $(LOG)/Pure-WWW_Find.gz
    2.14 +
    2.15 +all: test
    2.16 +test: $(LOGFILE)
    2.17 +
    2.18 +$(LOGFILE): echo.ML find_theorems.ML html_unicode.ML \
    2.19 +  http_status.ML http_util.ML mime.ML scgi_req.ML scgi_server.ML \
    2.20 +  socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
    2.21 +	cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
    2.22 +
    2.23 +clean:
    2.24 +	rm -f $(LOGFILE)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/WWW_Find/ROOT.ML	Fri Nov 20 18:36:44 2009 +1100
     3.3 @@ -0,0 +1,14 @@
     3.4 +if String.isPrefix "polyml" ml_system
     3.5 +then 
     3.6 +  (use "unicode_symbols.ML";
     3.7 +  use "html_unicode.ML";
     3.8 +  use "mime.ML";
     3.9 +  use "http_status.ML";
    3.10 +  use "http_util.ML";
    3.11 +  use "xhtml.ML";
    3.12 +  use "socket_util.ML";
    3.13 +  use "scgi_req.ML";
    3.14 +  use "scgi_server.ML";
    3.15 +  use "echo.ML";
    3.16 +  use "find_theorems.ML")
    3.17 +else ()
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/WWW_Find/doc/README	Fri Nov 20 18:36:44 2009 +1100
     4.3 @@ -0,0 +1,28 @@
     4.4 +Requirements
     4.5 +------------
     4.6 +  lighttpd
     4.7 +  polyml (other ML systems untested)
     4.8 +
     4.9 +Quick setup
    4.10 +-----------
    4.11 +*  install lighttpd if necessary
    4.12 +   (and optionally disable automatic startup on default www port)
    4.13 +
    4.14 +Quick instructions
    4.15 +------------------
    4.16 +* start the server with:
    4.17 +    isabelle wwwfind start
    4.18 +  (add -l for logging from ML)
    4.19 +
    4.20 +* connect (by default) on port 8000:
    4.21 +    http://localhost:8000/isabelle/find_theorems
    4.22 +
    4.23 +* test with the echo server:
    4.24 +    http://localhost:8000/isabelle/echo
    4.25 +
    4.26 +* check the status with:
    4.27 +    isabelle wwwfind status
    4.28 +
    4.29 +* stop the server with:
    4.30 +    isabelle wwwfind stop
    4.31 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/WWW_Find/doc/design.tex	Fri Nov 20 18:36:44 2009 +1100
     5.3 @@ -0,0 +1,330 @@
     5.4 +% $Id$
     5.5 +%
     5.6 +% vim:nojs: tw=76 sw=4 sts=4 fo=awn fdm=marker
     5.7 +%
     5.8 +% 20090406 T. Bourke
     5.9 +%	Original document.
    5.10 +%
    5.11 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    5.12 +\documentclass[a4paper,draft]{article} % XXX
    5.13 +%\documentclass[a4paper,final]{article}
    5.14 +% Preamble
    5.15 +\usepackage[T1]{fontenc}
    5.16 +\usepackage{textcomp}
    5.17 +\usepackage{ifdraft}
    5.18 +
    5.19 +\bibliographystyle{abbrv} % alpha
    5.20 +
    5.21 +\newcommand{\refsec}[1]{Section~\ref{sec:#1}}
    5.22 +\newcommand{\reffig}[1]{Figure~\ref{fig:#1}}
    5.23 +\newcommand{\reftab}[1]{Table~\ref{tab:#1}}
    5.24 +
    5.25 +%
    5.26 +\usepackage{acronym}
    5.27 +\usepackage{pst-all}
    5.28 +\usepackage{url}
    5.29 +
    5.30 +\title{Isabelle find\_theorems on the web}
    5.31 +\author{T. Bourke\thanks{NICTA}}
    5.32 +
    5.33 +\special{!/pdfmark where
    5.34 + {pop} {userdict /pdfmark /cleartomark load put} ifelse
    5.35 + [ /Author   (T. Bourke, NICTA)
    5.36 +   /Title    (IsabelleWWW: find_theorems
    5.37 +	      ($Date: 2008-10-03 16:09:02 +1000 (Fri, 03 Oct 2008) $))
    5.38 +   /Subject  (Web interface to find_theorems)
    5.39 +   /Keywords (isabelle, sml, http, www)
    5.40 +   /DOCINFO pdfmark}
    5.41 +
    5.42 +\begin{document}
    5.43 +% Title page and abstract
    5.44 +\maketitle
    5.45 +
    5.46 +\begin{abstract}
    5.47 +The Isabelle find\_theorems command processes queries against a theory 
    5.48 +database and returns a list of matching theorems.
    5.49 +It is usually given from the Proof General or command-line interface.
    5.50 +This document describes a web server implementation.
    5.51 +Two design alternatives are presented and an overview of an implementation 
    5.52 +of one is described.
    5.53 +\end{abstract}
    5.54 +
    5.55 +\section{Introduction}\label{sec:intro}
    5.56 +
    5.57 +This document describes the design and implementation of a web interface for 
    5.58 +the Isabelle find\_theorems command.
    5.59 +The design requirements and their consequences are detailed in \refsec{req}.
    5.60 +Two architectures were considered: \begin{enumerate}
    5.61 +
    5.62 +\item \emph{one process}: integrate a web server into Isabelle.
    5.63 +
    5.64 +\item \emph{two processes}: run Isabelle as a web server module.
    5.65 +
    5.66 +\end{enumerate}
    5.67 +A brief evaluation of the one process architecture is presented in 
    5.68 +\refsec{oneproc}.
    5.69 +An implementation of the two process is presented in \refsec{twoproc}.
    5.70 +
    5.71 +\section{Design requirements}\label{sec:req}
    5.72 +
    5.73 +The main requirements are:\begin{enumerate}
    5.74 +\item The system will allow users to search for theorems from a web browser.
    5.75 +\item It will allow queries across disparate Isabelle theories.
    5.76 +\item It will, at a minimum, handle theories from the L4.verified project.
    5.77 +\item It will run on a secure network.
    5.78 +\item There will be at most ten simultaneous users.
    5.79 +\end{enumerate}
    5.80 +
    5.81 +\noindent
    5.82 +Several \emph{a priori} choices are fixed:\begin{enumerate}
    5.83 +\item The search will run against an Isabelle heap.
    5.84 +\item A single heap will be built from the theories to be searched.
    5.85 +\item The system must be persistent, for two reasons: \begin{enumerate}
    5.86 +    \item Isabelle is slow to start against large heaps.
    5.87 +    \item Later enhancements may require tracking states at the server.
    5.88 +\end{enumerate}
    5.89 +\end{enumerate}
    5.90 +
    5.91 +\section{Evaluation: Isabelle web server}\label{sec:oneproc}
    5.92 +
    5.93 +The advantage of integrating a web server into Isabelle is that the 
    5.94 +find\_theorems service could be provided by a single process, which, in 
    5.95 +principle, would simplify administration.
    5.96 +Implementing even a simple \ac{HTTP} service from scratch is an unacceptable 
    5.97 +cost and fraught with potential problems and limitations.
    5.98 +It is preferable to adapt an existing system.
    5.99 +
   5.100 +As Isabelle is written in \ac{SML}, only \ac{HTTP} services also written in 
   5.101 +\ac{SML} can realistically be considered.
   5.102 +In principle Isabelle compiles on both Poly/ML and \ac{SML/NJ}, but in 
   5.103 +practice the former is faster, more widely used, and better supported.
   5.104 +In particular, the L4.verified project does not build effectively on 
   5.105 +\ac{SML/NJ}.
   5.106 +This further limits the potential to adapt an existing system.
   5.107 +
   5.108 +There are three \ac{SML} web server projects:\\
   5.109 +\centerline{\begin{tabular}{ll}
   5.110 +SMLServer &
   5.111 +    \url{http://www.smlserver.org}\\
   5.112 +FoxNet web server &
   5.113 +    \url{http://www.cs.cmu.edu/~fox/}\\
   5.114 +Swerve web server &
   5.115 +    \url{http://mlton.org/Swerve}
   5.116 +\end{tabular}}
   5.117 +
   5.118 +Unfortunately, none of these projects is suitable.
   5.119 +
   5.120 +The SMLServer is an Apache web server plugin.
   5.121 +It runs \ac{SML} programs that generate dynamic web pages.
   5.122 +SMLServer is based on the MLKit compiler.
   5.123 +It is unlikely that Isabelle and the l4.verified heaps could be compiled in 
   5.124 +MLKit, at least not without significant effort.
   5.125 +
   5.126 +The FoxNet web server was developed as part of the Fox project at \ac{CMU}.
   5.127 +The source is not readily available.
   5.128 +
   5.129 +The Swerve web server is part of an unpublished book on systems programming 
   5.130 +in \ac{SML}.
   5.131 +The source code is available and it is readily patched to run under the 
   5.132 +latest version of SML/NJ (110.67).
   5.133 +Adapting it to Poly/ML would require non-trivial effort because it is based 
   5.134 +on \ac{CML}, whose implementation on SML/NJ makes use of continuations 
   5.135 +(SMLofNJ.cont).
   5.136 +
   5.137 +\section{Implementation: Isabelle web module}\label{sec:twoproc}
   5.138 +
   5.139 +The description of the two process solution is divided into two subsections.
   5.140 +The first contains an overview of the architecture and web server specifics.
   5.141 +The second contains a summary of an \ac{SML} implementation of the web 
   5.142 +module in Isabelle.
   5.143 +
   5.144 +\subsection{Architecture and web server}\label{sec:oneproc:arch}
   5.145 +
   5.146 +\newcommand{\component}[1]{%
   5.147 +    \rput(0,0){\psframe(-.8,-.6)(.8,.6)}%
   5.148 +    \rput(0,0){\parbox{4.3em}{\centering{#1}}}}
   5.149 +
   5.150 +\begin{figure}
   5.151 +\centering%
   5.152 +\begin{pspicture}(-4.8,0)(3.3,4)%\psgrid
   5.153 +    \newpsstyle{conn}{arrows=->}%
   5.154 +    %
   5.155 +    \rput(-2.2,3.3){\component{web server}}%
   5.156 +    \rput( 2.2,3.3){\component{web module}}%
   5.157 +    \rput(-2.2,0.7){\component{web client}}%
   5.158 +    \rput(-4.2,3.4){%
   5.159 +	\psellipse(0,-.2)(.4,.2)%
   5.160 +	\psframe[linestyle=none,fillstyle=solid,fillcolor=white]%
   5.161 +		(-.4,-.2)(.4,.1)%
   5.162 +	\psellipse(0,.1)(.4,.2)%
   5.163 +	\psline(-.38,-.2)(-.38,.1)\psline(.38,-.2)(.38,.1)%
   5.164 +    }%
   5.165 +    \psline[style=conn,arrows=<->](-3.0,3.3)(-3.8,3.3)%
   5.166 +    %
   5.167 +    \rput[rB](3.3,2.15){server}%
   5.168 +    \psline[linestyle=dashed](-4.8,2)(3.3,2)%
   5.169 +    \rput[rt](3.3,1.90){network}%
   5.170 +    %
   5.171 +    \rput[B](0.0,3.55){\psframebox*{module protocol}}%
   5.172 +    \psline[style=conn](-1.4,3.4)(1.4,3.4)%
   5.173 +    \psline[style=conn](1.4,3.2)(-1.4,3.2)%
   5.174 +    %
   5.175 +    \rput[B]{90}(-2.4,2.0){\psframebox*{\ac{HTTP}}}%
   5.176 +    \psline[style=conn](-2.1,2.7)(-2.1,1.3)%
   5.177 +    \psline[style=conn](-2.3,1.3)(-2.3,2.7)%
   5.178 +\end{pspicture}
   5.179 +\caption{Overview of web module architecture\label{fig:modulearch}}
   5.180 +\end{figure}
   5.181 +
   5.182 +An overview of a simple web server architecture is presented in 
   5.183 +\reffig{modulearch}.
   5.184 +A \emph{web client} requests a \ac{URL} from a \emph{web server} over 
   5.185 +\ac{HTTP}.
   5.186 +The web server processes the request by fetching static elements from its 
   5.187 +local file system and communicating with \emph{web modules} to dynamically 
   5.188 +generate other elements.
   5.189 +The elements are sent back across the network to the web client.
   5.190 +
   5.191 +The web server communicates with web modules over a \emph{module protocol}, 
   5.192 +which dictates a means of passing requests and receiving responses.
   5.193 +There are several common module protocols.
   5.194 +
   5.195 +In the \ac{CGI}, the web server executes processes to service dynamic 
   5.196 +\acp{URL}.
   5.197 +Request details are placed in environment variables and sent on the standard 
   5.198 +input channels of processes, responses are read from the standard output 
   5.199 +channels of processes and transmitted back to web clients.
   5.200 +
   5.201 +The chief disadvantage of \ac{CGI} is that it creates a new process for 
   5.202 +every request.
   5.203 +Fast \ac{CGI} web modules, on the other hand, run persistently in a loop.
   5.204 +They receive and respond to web server requests over a duplex socket.
   5.205 +The Fast \ac{CGI} protocol is quite complicated.
   5.206 +There are, however, alternatives like \ac{SCGI} that are easier for web 
   5.207 +modules to support.
   5.208 +This is important when programming in \ac{SML} because both the number of 
   5.209 +developers and available libraries are small.
   5.210 +
   5.211 +An \ac{SCGI} web module listens on a socket for requests from a web server.
   5.212 +Requests are sent as stream of bytes.
   5.213 +The first part of the request is a null-delimited sequence of name and value 
   5.214 +pairs.
   5.215 +The second part is unparsed text sent from the web client.
   5.216 +The web module responds by sending text, usually \ac{HTTP} headers followed 
   5.217 +by \ac{HTML} data, back over the socket.
   5.218 +The whole protocol can be described in two 
   5.219 +pages.\footnote{\url{http://python.ca/scgi/protocol.txt}}
   5.220 +
   5.221 +Both the Apache and Lighttpd web servers support the \ac{SCGI} protocol.
   5.222 +Lighttpd was chosen because it seemed to be small, fast, and easy to 
   5.223 +configure.
   5.224 +Two settings are required to connect lighttpd to an \ac{SCGI} web module: 
   5.225 +\begin{verbatim}
   5.226 +server.modules = ( "mod_scgi" )
   5.227 +scgi.server = ("/isabelle" => ((
   5.228 +		  "host" => "127.0.0.1",
   5.229 +		  "port" => 64000,
   5.230 +		  "check-local" => "disable")))
   5.231 +\end{verbatim}
   5.232 +In this example, the \texttt{scgi.server} entry directs the web server to 
   5.233 +pass all \acp{URL} beginning with \texttt{/isabelle} to the web module 
   5.234 +listening on port \texttt{64000}.
   5.235 +
   5.236 +\subsection{Implementation in \acs{SML}}\label{sec:oneproc:impl}
   5.237 +
   5.238 +\begin{table}
   5.239 +\begin{tabular}{lp{.70\textwidth}}
   5.240 +\textbf{Module}	     &	\textbf{Description}\\\hline
   5.241 +Mime		     &	Rudimentary support for mime types.\\
   5.242 +HttpStatus	     &	\ac{HTTP} header status codes.\\
   5.243 +HttpUtil	     &	Produce \ac{HTTP} headers and parse query strings.\\
   5.244 +Xhtml		     &	Rudimentary support for generating \ac{HTML}.\\
   5.245 +SocketUtil	     &	Routines from The Standard ML Basis Library
   5.246 +			book.\footnote{Chapter 10, Gansner and Reppy, 
   5.247 +			Cambridge University Press.}\\
   5.248 +\textbf{ScgiReq}     &	Parse \ac{SCGI} requests.\\
   5.249 +\textbf{ScgiServer}  &	\ac{SCGI} server event loop and dispatch.\\
   5.250 +\textbf{FindTheorems}&	\ac{HTML} interface to find\_theorems.
   5.251 +\end{tabular}
   5.252 +\caption{Web module implementation\label{tab:moduleimpl}}
   5.253 +\end{table}
   5.254 +
   5.255 +The find\_theorems web module is implemented in \ac{SML}.
   5.256 +It uses elements of the Pure library in Isabelle.
   5.257 +The program comprises the nine modules shown in \reftab{moduleimpl}.
   5.258 +The three most important ones are shown in bold: ScgiReq, ScgiServer, and 
   5.259 +FindTheorems.
   5.260 +
   5.261 +ScgiReq implements the client-side of the \ac{SCGI} protocol.
   5.262 +It maps a binary input stream into a request data type.
   5.263 +
   5.264 +ScgiServer is a generic, multi-threaded \ac{SCGI} request dispatcher.
   5.265 +It accepts \ac{SCGI} requests on a designated socket, selects an appropriate 
   5.266 +handler from an internal list, and calls the handler in a new thread.
   5.267 +
   5.268 +FindTheorems registers a handler with ScgiServer.
   5.269 +It parses \ac{SCGI}/\ac{HTTP} requests, calls the Isabelle find\_theorems 
   5.270 +function, and returns the results as \ac{HTML}.
   5.271 +The \ac{HTML} generation of individual theorems is handled by the \ac{HTML} 
   5.272 +print mode of Isabelle, but the form fields and page structure were manually 
   5.273 +implemented.
   5.274 +
   5.275 +The module is built by using a \texttt{ROOT.ML} file inside a heap that 
   5.276 +contains the theories to be searched.
   5.277 +The server is started by calling \texttt{ScgiServer.server}.
   5.278 +Scripts have been created to automate this process.
   5.279 +
   5.280 +\subsection{Handling symbols}\label{sec:unicode}
   5.281 +
   5.282 +Isabelle theorems are usually written in mathematical notation.
   5.283 +Internally, however, Isabelle only manipulates \acs{ASCII} strings.
   5.284 +Symbols are encoded by strings that begin with a backslash and contain a 
   5.285 +symbol name between angle braces, for example, the symbol~$\longrightarrow$ 
   5.286 +becomes~\verb+\<longrightarrow>+.
   5.287 +The existing Thy/Html module in the Isabelle Pure theory converts many of 
   5.288 +these symbols to \ac{HTML} entities.
   5.289 +Custom routines are required to convert the missing symbols to \ac{HTML} 
   5.290 +\emph{numeric character references}, which are the Unicode codepoints of 
   5.291 +symbols printed in decimal between \verb+&#+ and \verb+;+.
   5.292 +Further, other routines were required for converting \acs{UTF-8} encoded 
   5.293 +strings sent from web browsers into Isabelle's symbol encoding.
   5.294 +
   5.295 +Isabelle is distributed with a text file that maps Isabelle symbols to 
   5.296 +Unicode codepoints.
   5.297 +A module was written to parse this file into symbol tables that map back and 
   5.298 +forth between Isabelle symbols and Unicode codepoints, and also between 
   5.299 +Isabelle \acs{ASCII} abbreviations (like \verb+-->+ for $\longrightarrow$) 
   5.300 +and Unicode codepoints.
   5.301 +
   5.302 +The conversion from Isabelle symbols to \ac{HTML} numeric character 
   5.303 +references is handled by a new printing mode, which is based in large part 
   5.304 +on the existing \ac{HTML} printing mode.
   5.305 +The new mode is used in combination with the existing \texttt{xsymbol} mode, 
   5.306 +to ensure that Isabelle symbols are used instead of \acs{ASCII} 
   5.307 +abbreviations.
   5.308 +
   5.309 +The conversion from \acs{UTF-8} is handled by a custom routine.
   5.310 +Additionally, there is a JavaScript routine that converts from Isabelle 
   5.311 +symbol encodings to \acs{UTF-8}, so that users can conveniently view 
   5.312 +manually-entered or pasted mathematical characters in the web browser 
   5.313 +interface.
   5.314 +
   5.315 +\section{Abbreviations}\label{sec:abbr}
   5.316 +
   5.317 +\begin{acronym}[SML/NJ] % longest acronym here
   5.318 +    \acro{ASCII}{American Standard Code for Information Interchange}
   5.319 +    \acro{CGI}{Common Gateway Interface}
   5.320 +    \acro{CML}{Concurrent ML}
   5.321 +    \acro{CMU}{Carnegie Mellon University}
   5.322 +    \acro{HTML}{Hyper Text Markup Language}
   5.323 +    \acro{HTTP}{Hyper Text Transfer Protocol}
   5.324 +    \acro{ML}{Meta Language}
   5.325 +    \acro{SCGI}{Simple CGI}
   5.326 +    \acro{SML}{Standard ML}
   5.327 +    \acro{SML/NJ}{Standard ML of New Jersey}
   5.328 +    \acro{URL}{Universal Resource Locator}
   5.329 +    \acro{UTF-8}{8-bit Unicode Transformation Format}
   5.330 +    \acro{WWW}{World Wide Web}
   5.331 +\end{acronym}
   5.332 +
   5.333 +\end{document}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/WWW_Find/echo.ML	Fri Nov 20 18:36:44 2009 +1100
     6.3 @@ -0,0 +1,16 @@
     6.4 +(*  Title:      echo.ML
     6.5 +    Author:     Timothy Bourke, NICTA
     6.6 +
     6.7 +    Install simple echo server.
     6.8 +*)
     6.9 +
    6.10 +local
    6.11 +fun echo (req, content, send) =
    6.12 +  (send (ScgiReq.show req);
    6.13 +   send "--payload-----\n";
    6.14 +   send (Byte.bytesToString content);
    6.15 +   send "\n--------------\n")
    6.16 +in
    6.17 +val () = ScgiServer.register ("echo", SOME Mime.plain, echo);
    6.18 +end;
    6.19 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/WWW_Find/etc/settings	Fri Nov 20 18:36:44 2009 +1100
     7.3 @@ -0,0 +1,7 @@
     7.4 +# the path to lighttpd
     7.5 +LIGHTTPD="/usr/sbin/lighttpd"
     7.6 +
     7.7 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     7.8 +
     7.9 +WWWFINDDIR="$COMPONENT"
    7.10 +WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Nov 20 18:36:44 2009 +1100
     8.3 @@ -0,0 +1,244 @@
     8.4 +(*  Title:      find_theorems.ML
     8.5 +    Author:     Timothy Bourke, NICTA
     8.6 +
     8.7 +    Simple find_theorems server
     8.8 +*)
     8.9 +
    8.10 +local
    8.11 +val default_limit = 20;
    8.12 +val thy_names = sort string_ord (ThyInfo.get_names ());
    8.13 +
    8.14 +val find_theorems_url = "find_theorems";
    8.15 +
    8.16 +fun is_sorry thm =
    8.17 +  Thm.proof_of thm
    8.18 +  |> Proofterm.approximate_proof_body
    8.19 +  |> Proofterm.all_oracles_of
    8.20 +  |> exists (fn (x, _) => x = "Pure.skip_proof");
    8.21 +
    8.22 +local open Xhtml in
    8.23 +fun find_theorems_form thy_name (query, limit, withdups) =
    8.24 +  let
    8.25 +    val query_input =
    8.26 +      input (id "query", {
    8.27 +        name = "query",
    8.28 +        itype = TextInput { value = query, maxlength = NONE }});
    8.29 +
    8.30 +    val max_results = divele noid
    8.31 +      [
    8.32 +        label (noid, { for = "limit" }, "Max. results:"),
    8.33 +        input (id "limit",
    8.34 +          { name = "limit",
    8.35 +            itype = TextInput { value = SOME (Int.toString limit),
    8.36 +                                maxlength = NONE }})
    8.37 +      ];
    8.38 +
    8.39 +    val theories = divele noid
    8.40 +      [
    8.41 +        label (noid, { for = "theory" }, "Search in:"),
    8.42 +        select (id "theory", { name = "theory", value = SOME thy_name })
    8.43 +               thy_names
    8.44 +      ];
    8.45 +
    8.46 +    val with_dups = divele noid
    8.47 +      [
    8.48 +        label (noid, { for = "withdups" }, "Allow duplicates:"),
    8.49 +        input (id "withdups",
    8.50 +          { name = "withdups",
    8.51 +            itype = Checkbox { checked = withdups, value = SOME "true" }})
    8.52 +      ];
    8.53 +
    8.54 +    val help = divele (class "help")
    8.55 +      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
    8.56 +  in
    8.57 +    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
    8.58 +      [tag "fieldset" []
    8.59 +        [tag "legend" [] [text "find_theorems"],
    8.60 +         (add_script (OnKeyPress, "encodequery(this)")
    8.61 +          o add_script (OnChange, "encodequery(this)")
    8.62 +          o add_script (OnMouseUp, "encodequery(this)")) query_input,
    8.63 +         divele (class "settings") [ max_results, theories, with_dups, help ],
    8.64 +         divele (class "mainbuttons")
    8.65 +           [ reset_button (id "reset"), submit_button (id "submit") ]
    8.66 +        ]
    8.67 +      ]
    8.68 +  end;
    8.69 +
    8.70 +fun html_header thy_name args =
    8.71 +  html { lang = "en" } [
    8.72 +    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
    8.73 +         [script (noid, { script_type="text/javascript",
    8.74 +                          src="/find_theorems.js" })],
    8.75 +    add_script (OnLoad, "encodequery(document.getElementById('query'))")
    8.76 +      (body noid [
    8.77 +          h (noid, 1, "Theory " ^ thy_name),
    8.78 +          find_theorems_form thy_name args,
    8.79 +          divele noid []
    8.80 +         ])
    8.81 +  ];
    8.82 +
    8.83 +fun html_error msg = p ((class "error"), msg);
    8.84 +
    8.85 +val find_theorems_table =
    8.86 +  table (class "findtheorems")
    8.87 +    [
    8.88 +      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
    8.89 +      tbody noid []
    8.90 +    ];
    8.91 +
    8.92 +fun show_criterion (b, c) =
    8.93 +  let
    8.94 +    fun prfx s = let
    8.95 +        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
    8.96 +      in span (class c, v) end;
    8.97 +
    8.98 +    fun prfxwith s = let
    8.99 +        val (c, v) =
   8.100 +          if b
   8.101 +          then ("criterion", "with " ^ s)
   8.102 +          else ("ncriterion", "without " ^ s);
   8.103 +      in span (class c, v) end;
   8.104 +  in
   8.105 +    (case c of
   8.106 +      Find_Theorems.Name name => prfx ("name: " ^ quote name)
   8.107 +    | Find_Theorems.Intro => prfx "intro"
   8.108 +    | Find_Theorems.IntroIff => prfx "introiff"
   8.109 +    | Find_Theorems.Elim => prfx "elim"
   8.110 +    | Find_Theorems.Dest => prfx "dest"
   8.111 +    | Find_Theorems.Solves => prfx "solves"
   8.112 +    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
   8.113 +    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
   8.114 +  end;
   8.115 +
   8.116 +fun find_theorems_summary (othmslen, thmslen, query, args) =
   8.117 +  let
   8.118 +    val args =
   8.119 +      (case othmslen of
   8.120 +         NONE => args
   8.121 +       | SOME l => Symtab.update ("limit", Int.toString l) args)
   8.122 +    val qargs = HttpUtil.make_query_string args;
   8.123 +
   8.124 +    val num_found_text =
   8.125 +      (case othmslen of
   8.126 +         NONE => text (Int.toString thmslen)
   8.127 +       | SOME l =>
   8.128 +           a { href = find_theorems_url ^
   8.129 +               (if qargs = "" then "" else "?" ^ qargs),
   8.130 +           text = Int.toString l })
   8.131 +    val found = [text "found ", num_found_text, text " theorems"] : tag list;
   8.132 +    val displayed =
   8.133 +      if is_some othmslen
   8.134 +      then " (" ^ Int.toString thmslen ^ " displayed)"
   8.135 +      else "";
   8.136 +    fun show_search c = tr [ td' noid [show_criterion c] ];
   8.137 +  in
   8.138 +    table (class "findtheoremsquery")
   8.139 +    (* [ tr [ th (noid, "searched for:") ] ]
   8.140 +       @ map show_search query @ *)
   8.141 +      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
   8.142 +  end
   8.143 +
   8.144 +fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
   8.145 +
   8.146 +fun html_thm ctxt (n, (thmref, thm)) =
   8.147 +  let
   8.148 +    val string_of_thm =
   8.149 +      Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
   8.150 +        setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
   8.151 +  in
   8.152 +    tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
   8.153 +      [
   8.154 +        tag' "td" (class "name")
   8.155 +          [span' (sorry_class thm)
   8.156 +             [raw_text (Facts.string_of_ref thmref)]
   8.157 +          ],
   8.158 +        tag' "td" (class "thm") [pre noid (string_of_thm thm)]
   8.159 +      ]
   8.160 +  end;
   8.161 +
   8.162 +end;
   8.163 +
   8.164 +structure P = OuterParse
   8.165 +      and K = OuterKeyword
   8.166 +      and FT = Find_Theorems;
   8.167 +
   8.168 +val criterion =
   8.169 +  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
   8.170 +  P.reserved "intro" >> K Find_Theorems.Intro ||
   8.171 +  P.reserved "elim" >> K Find_Theorems.Elim ||
   8.172 +  P.reserved "dest" >> K Find_Theorems.Dest ||
   8.173 +  P.reserved "solves" >> K Find_Theorems.Solves ||
   8.174 +  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
   8.175 +  P.term >> Find_Theorems.Pattern;
   8.176 +
   8.177 +val parse_query =
   8.178 +  Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
   8.179 +
   8.180 +fun app_index f xs = fold_index (fn x => K (f x)) xs ();
   8.181 +
   8.182 +fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
   8.183 +                   content, send) =
   8.184 +  let
   8.185 +    val arg_data =
   8.186 +      (case request_method of
   8.187 +         ScgiReq.Get => query_string
   8.188 +       | ScgiReq.Post =>
   8.189 +          content
   8.190 +          |> Byte.bytesToString
   8.191 +          |> HttpUtil.parse_query_string
   8.192 +       | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
   8.193 +
   8.194 +    val args = Symtab.lookup arg_data;
   8.195 +
   8.196 +    val query = the_default "" (args "query");
   8.197 +    fun get_query () =
   8.198 +      query
   8.199 +      |> (fn s => s ^ ";")
   8.200 +      |> OuterSyntax.scan Position.start
   8.201 +      |> filter OuterLex.is_proper
   8.202 +      |> Scan.error parse_query
   8.203 +      |> fst;
   8.204 +
   8.205 +    val limit =
   8.206 +      args "limit"
   8.207 +      |> Option.mapPartial Int.fromString
   8.208 +      |> the_default default_limit;
   8.209 +    val thy_name =
   8.210 +      args "theory"
   8.211 +      |> the_default "Main";
   8.212 +    val with_dups = is_some (args "with_dups");
   8.213 +
   8.214 +    fun do_find () =
   8.215 +      let
   8.216 +        val ctxt = ProofContext.init (theory thy_name);
   8.217 +        val query = get_query ();
   8.218 +        val (othmslen, thms) = apsnd rev
   8.219 +          (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
   8.220 +        val thmslen = length thms;
   8.221 +        fun thm_row args = Xhtml.write send (html_thm ctxt args);
   8.222 +      in
   8.223 +        Xhtml.write send
   8.224 +          (find_theorems_summary (othmslen, thmslen, query, arg_data));
   8.225 +        if null thms then ()
   8.226 +        else (Xhtml.write_open send find_theorems_table;
   8.227 +              HTML_Unicode.print_mode (app_index thm_row) thms;
   8.228 +              Xhtml.write_close send find_theorems_table)
   8.229 +      end;
   8.230 +
   8.231 +    val header = (html_header thy_name (args "query", limit, with_dups));
   8.232 +  in
   8.233 +    send Xhtml.doctype_xhtml1_0_strict;
   8.234 +    Xhtml.write_open send header;
   8.235 +    if query = "" then ()
   8.236 +    else
   8.237 +      do_find ()
   8.238 +        handle
   8.239 +          ERROR msg => Xhtml.write send (html_error msg)
   8.240 +        | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
   8.241 +    Xhtml.write_close send header
   8.242 +  end;
   8.243 +in
   8.244 +val () = show_question_marks := false;
   8.245 +val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
   8.246 +end;
   8.247 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Fri Nov 20 18:36:44 2009 +1100
     9.3 @@ -0,0 +1,85 @@
     9.4 +(*  Title:      html_unicode.ML
     9.5 +    Author:     Timothy Bourke, NICTA
     9.6 +                Based on Pure/Thy/html.ML
     9.7 +                by Markus Wenzel and Stefan Berghofer, TU Muenchen
     9.8 +
     9.9 +HTML presentation elements that use unicode code points.
    9.10 +*)
    9.11 +
    9.12 +signature HTML_UNICODE =
    9.13 +sig
    9.14 +  val print_mode: ('a -> 'b) -> 'a -> 'b
    9.15 +end;
    9.16 +
    9.17 +structure HTML_Unicode: HTML_UNICODE =
    9.18 +struct
    9.19 +
    9.20 +(** HTML print modes **)
    9.21 +
    9.22 +(* mode *)
    9.23 +
    9.24 +val htmlunicodeN = "HTMLUnicode";
    9.25 +fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
    9.26 +
    9.27 +(* symbol output *)
    9.28 +
    9.29 +local
    9.30 +  val sym_width_lookup = Symtab.make
    9.31 +   [("\<spacespace>", 2),
    9.32 +    ("\<Longleftarrow>", 2),
    9.33 +    ("\<longleftarrow>", 2),
    9.34 +    ("\<Longrightarrow>", 2),
    9.35 +    ("\<longrightarrow>", 2),
    9.36 +    ("\<longleftrightarrow>", 2),
    9.37 +    ("\<^bsub>", 0),
    9.38 +    ("\<^esub>", 0),
    9.39 +    ("\<^bsup>", 0),
    9.40 +    ("\<^esup>", 0)];
    9.41 +
    9.42 +  fun sym_width s =
    9.43 +    (case Symtab.lookup sym_width_lookup s of
    9.44 +       NONE => 1
    9.45 +     | SOME w => w);
    9.46 +
    9.47 +  fun output_sym s =
    9.48 +    if Symbol.is_raw s then (1, Symbol.decode_raw s)
    9.49 +    else
    9.50 +      (case UnicodeSymbols.symbol_to_unicode s of
    9.51 +         SOME x => (sym_width s, "&#" ^ Int.toString x ^ ";") (* numeric entities *)
    9.52 +         (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x])     (* utf-8 *) *)
    9.53 +       | NONE => (size s, XML.text s));
    9.54 +
    9.55 +  fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
    9.56 +  fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
    9.57 +  fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
    9.58 +
    9.59 +  fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
    9.60 +    | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
    9.61 +    | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
    9.62 +    | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
    9.63 +    | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
    9.64 +    | output_syms (s :: ss) = output_sym s :: output_syms ss
    9.65 +    | output_syms [] = [];
    9.66 +
    9.67 +  fun output_width str =
    9.68 +    if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
    9.69 +    then Output.default_output str
    9.70 +    else
    9.71 +      let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
    9.72 +        (output_syms (Symbol.explode str)) 0
    9.73 +      in (implode syms, width) end;
    9.74 +in
    9.75 +
    9.76 +val output = #1 o output_width;
    9.77 +
    9.78 +val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw;
    9.79 +
    9.80 +end;
    9.81 +
    9.82 +(* common markup *)
    9.83 +
    9.84 +fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
    9.85 +
    9.86 +val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name);
    9.87 +
    9.88 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/WWW_Find/http_status.ML	Fri Nov 20 18:36:44 2009 +1100
    10.3 @@ -0,0 +1,157 @@
    10.4 +(*  Title:      http_status.ML
    10.5 +    Author:     Timothy Bourke, NICTA
    10.6 +
    10.7 +HTTP status codes and reasons.
    10.8 +*)
    10.9 +signature HTTP_STATUS =
   10.10 +sig
   10.11 +  type t
   10.12 +
   10.13 +  val to_status_code : t -> int
   10.14 +  val to_reason : t -> string
   10.15 +  val from_status_code : int -> t option
   10.16 +
   10.17 +  val continue : t
   10.18 +  val switching_protocols : t
   10.19 +  val ok : t
   10.20 +  val created : t
   10.21 +  val accepted : t
   10.22 +  val non_authoritative_information : t
   10.23 +  val no_content : t
   10.24 +  val reset_content : t
   10.25 +  val partial_content : t
   10.26 +  val multiple_choices : t
   10.27 +  val moved_permanently : t
   10.28 +  val found : t
   10.29 +  val see_other : t
   10.30 +  val not_modified : t
   10.31 +  val use_proxy : t
   10.32 +  val temporary_redirect : t
   10.33 +  val bad_request : t
   10.34 +  val unauthorized : t
   10.35 +  val payment_required : t
   10.36 +  val forbidden : t
   10.37 +  val not_found : t
   10.38 +  val method_not_allowed : t
   10.39 +  val not_acceptable : t
   10.40 +  val proxy_authentication_required : t
   10.41 +  val request_timeout : t
   10.42 +  val conflict : t
   10.43 +  val gone : t
   10.44 +  val length_required : t
   10.45 +  val precondition_failed : t
   10.46 +  val request_entity_too_large : t
   10.47 +  val request_uri_too_long : t
   10.48 +  val unsupported_media_type : t
   10.49 +  val requested_range_not_satisfiable : t
   10.50 +  val expectation_failed : t
   10.51 +  val internal_server_error : t
   10.52 +  val not_implemented : t
   10.53 +  val bad_gateway : t
   10.54 +  val service_unavailable : t
   10.55 +  val gateway_timeout : t
   10.56 +  val http_version_not_supported : t
   10.57 +
   10.58 +end;
   10.59 +
   10.60 +structure HttpStatus : HTTP_STATUS =
   10.61 +struct
   10.62 +
   10.63 +type t = int
   10.64 +
   10.65 +local
   10.66 +val int_status_map = Inttab.make
   10.67 +  [(100, "Continue"),
   10.68 +   (101, "Switching Protocols"),
   10.69 +   (200, "OK"),
   10.70 +   (201, "Created"),
   10.71 +   (202, "Accepted"),
   10.72 +   (203, "Non-Authoritative Information"),
   10.73 +   (204, "No Content"),
   10.74 +   (205, "Reset Content"),
   10.75 +   (206, "Partial Content"),
   10.76 +   (300, "Multiple Choices"),
   10.77 +   (301, "Moved Permanently"),
   10.78 +   (302, "Found"),
   10.79 +   (303, "See Other"),
   10.80 +   (304, "Not Modified"),
   10.81 +   (305, "Use Proxy"),
   10.82 +   (307, "Temporary Redirect"),
   10.83 +   (400, "Bad Request"),
   10.84 +   (401, "Unauthorized"),
   10.85 +   (402, "Payment Required"),
   10.86 +   (403, "Forbidden"),
   10.87 +   (404, "Not Found"),
   10.88 +   (405, "Method Not Allowed"),
   10.89 +   (406, "Not Acceptable"),
   10.90 +   (407, "Proxy Authentication Required"),
   10.91 +   (408, "Request Timeout"),
   10.92 +   (409, "Conflict"),
   10.93 +   (410, "Gone"),
   10.94 +   (411, "Length Required"),
   10.95 +   (412, "Precondition Failed"),
   10.96 +   (413, "Request Entity Too Large"),
   10.97 +   (414, "Request URI Too Long"),
   10.98 +   (415, "Unsupported Media Type"),
   10.99 +   (416, "Requested Range Not Satisfiable"),
  10.100 +   (417, "Expectation Failed"),
  10.101 +   (500, "Internal Server Error"),
  10.102 +   (501, "Not Implemented"),
  10.103 +   (502, "Bad Gateway"),
  10.104 +   (503, "Service Unavailable"),
  10.105 +   (504, "Gateway Timeout"),
  10.106 +   (505, "HTTP Version Not Supported")];
  10.107 +in
  10.108 +fun from_status_code i =
  10.109 +  if is_some (Inttab.lookup int_status_map i)
  10.110 +  then SOME i
  10.111 +  else NONE;
  10.112 +
  10.113 +val to_reason = the o Inttab.lookup int_status_map;
  10.114 +end;
  10.115 +
  10.116 +val to_status_code = I;
  10.117 +
  10.118 +val continue = 100;
  10.119 +val switching_protocols = 101;
  10.120 +val ok = 200;
  10.121 +val created = 201;
  10.122 +val accepted = 202;
  10.123 +val non_authoritative_information = 203;
  10.124 +val no_content = 204;
  10.125 +val reset_content = 205;
  10.126 +val partial_content = 206;
  10.127 +val multiple_choices = 300;
  10.128 +val moved_permanently = 301;
  10.129 +val found = 302;
  10.130 +val see_other = 303;
  10.131 +val not_modified = 304;
  10.132 +val use_proxy = 305;
  10.133 +val temporary_redirect = 307;
  10.134 +val bad_request = 400;
  10.135 +val unauthorized = 401;
  10.136 +val payment_required = 402;
  10.137 +val forbidden = 403;
  10.138 +val not_found = 404;
  10.139 +val method_not_allowed = 405;
  10.140 +val not_acceptable = 406;
  10.141 +val proxy_authentication_required = 407;
  10.142 +val request_timeout = 408;
  10.143 +val conflict = 409;
  10.144 +val gone = 410;
  10.145 +val length_required = 411;
  10.146 +val precondition_failed = 412;
  10.147 +val request_entity_too_large = 413;
  10.148 +val request_uri_too_long = 414;
  10.149 +val unsupported_media_type = 415;
  10.150 +val requested_range_not_satisfiable = 416;
  10.151 +val expectation_failed = 417;
  10.152 +val internal_server_error = 500;
  10.153 +val not_implemented = 501;
  10.154 +val bad_gateway = 502;
  10.155 +val service_unavailable = 503;
  10.156 +val gateway_timeout = 504;
  10.157 +val http_version_not_supported = 505;
  10.158 +
  10.159 +end;
  10.160 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/WWW_Find/http_util.ML	Fri Nov 20 18:36:44 2009 +1100
    11.3 @@ -0,0 +1,94 @@
    11.4 +(*  Title:      http_util.ML
    11.5 +    Author:     Timothy Bourke, NICTA
    11.6 +
    11.7 +Rudimentary utility functions for HTTP.
    11.8 +*)
    11.9 +signature HTTP_UTIL =
   11.10 +sig
   11.11 +  val crlf : string
   11.12 +  val reply_header : HttpStatus.t * Mime.t option * (string * string) list -> string
   11.13 +  val parse_query_string : string -> string Symtab.table
   11.14 +  val make_query_string : string Symtab.table -> string
   11.15 +end;
   11.16 +
   11.17 +structure HttpUtil : HTTP_UTIL =
   11.18 +struct
   11.19 +
   11.20 +val crlf = "\r\n";
   11.21 +
   11.22 +fun make_header_field (name, value) = concat [name, ": ", value, crlf];
   11.23 +
   11.24 +fun reply_header (status, content_type, extra_fields) =
   11.25 +  let
   11.26 +    val code = (Int.toString o HttpStatus.to_status_code) status;
   11.27 +    val reason = HttpStatus.to_reason status;
   11.28 +    val show_content_type = pair "Content-Type" o Mime.show_type;
   11.29 +  in
   11.30 +  concat
   11.31 +    (map make_header_field
   11.32 +      (("Status", concat [code, " ", reason])
   11.33 +       :: (the_list o Option.map show_content_type) content_type
   11.34 +       @ extra_fields)
   11.35 +    @ [crlf])
   11.36 +  end;
   11.37 +
   11.38 +val split_fields = Substring.splitl (fn c => c <> #"=")
   11.39 +                   #> apsnd (Substring.triml 1);
   11.40 +
   11.41 +fun decode_url s =
   11.42 +  let
   11.43 +    fun to_char c =
   11.44 +      Substring.triml 1 c
   11.45 +      |> Int.scan StringCvt.HEX Substring.getc
   11.46 +      |> the
   11.47 +      |> fst
   11.48 +      |> Char.chr
   11.49 +      |> String.str
   11.50 +      |> Substring.full
   11.51 +      handle Option => c;
   11.52 +
   11.53 +    fun f (done, s) =
   11.54 +      let
   11.55 +        val (pre, post) = Substring.splitl (Char.notContains "+%") s;
   11.56 +      in
   11.57 +        if Substring.isEmpty post
   11.58 +        then (Substring.concat o rev) (pre::done)
   11.59 +        else
   11.60 +          if Substring.first post = SOME #"+"
   11.61 +            (* Substring.isPrefix "+" post *)(* seg fault in Poly/ML 5.1 *)
   11.62 +          then f (Substring.full " "::pre::done, Substring.triml 1 post)
   11.63 +          else let
   11.64 +            val (c, rest) = Substring.splitAt (post, 3)
   11.65 +                            handle Subscript =>
   11.66 +                              (Substring.full "%25", Substring.triml 1 post);
   11.67 +          in f (to_char c::pre::done, rest) end
   11.68 +      end;
   11.69 +  in f ([], s) end;
   11.70 +
   11.71 +val parse_query_string =
   11.72 +  Substring.full
   11.73 +  #> Substring.tokens (Char.contains "&;")
   11.74 +  #> map split_fields
   11.75 +  #> map (pairself (UnicodeSymbols.utf8_to_symbols o decode_url))
   11.76 +  #> distinct ((op =) o pairself fst)
   11.77 +  #> Symtab.make;
   11.78 +
   11.79 +local
   11.80 +fun to_entity #" " = "+"
   11.81 +  | to_entity c =
   11.82 +      if Char.isAlphaNum c orelse Char.contains ".-~_" c
   11.83 +      then String.str c
   11.84 +      else "%" ^ Int.fmt StringCvt.HEX (Char.ord c);
   11.85 +in
   11.86 +val encode_url = Substring.translate to_entity o Substring.full;
   11.87 +end
   11.88 +
   11.89 +fun join_pairs (n, v) = encode_url n ^ "=" ^ encode_url v;
   11.90 +
   11.91 +val make_query_string =
   11.92 +  Symtab.dest
   11.93 +  #> map join_pairs
   11.94 +  #> String.concatWith "&";
   11.95 +
   11.96 +end;
   11.97 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Fri Nov 20 18:36:44 2009 +1100
    12.3 @@ -0,0 +1,135 @@
    12.4 +#!/usr/bin/env bash
    12.5 +#
    12.6 +# Author: Timothy Bourke, NICTA
    12.7 +#         Based on scripts by Makarius Wenzel, TU Muenchen
    12.8 +#
    12.9 +# DESCRIPTION: run find theorems web server
   12.10 + 
   12.11 +PRG=$(basename "$0")
   12.12 +
   12.13 +function usage()
   12.14 +{
   12.15 +  echo
   12.16 +  echo "Usage: $ISABELLE_TOOL $PRG [Command] [Options] [HEAP]"
   12.17 +  echo
   12.18 +  echo "  Command must be one of:"
   12.19 +  echo "    start        start lighttpd and isabelle"
   12.20 +  echo "    stop         stop lighttpd and isabelle"
   12.21 +  echo "    status       show www and scgi port statuses"
   12.22 +  echo
   12.23 +  echo "  Options are:"
   12.24 +  echo "    -l		 make log file"
   12.25 +  echo "    -c           specify lighttpd config file"
   12.26 +  echo "                 (default: $WWWCONFIG)"
   12.27 +  echo
   12.28 +  echo "  Provide a web interface to find_theorems against the given HEAP"
   12.29 +  echo
   12.30 +  exit 1
   12.31 +}
   12.32 +
   12.33 +function fail()
   12.34 +{
   12.35 +  echo "$1" >&2
   12.36 +  exit 2
   12.37 +}
   12.38 +
   12.39 +function kill_by_port () {
   12.40 +  IPADDR='[0-9]*\.[0-9]*\.[0-9]*\.[0-9]*'
   12.41 +  PID=$(netstat -nltp 2>/dev/null \
   12.42 +        | sed -ne "s#^.*${IPADDR}:$1 *${IPADDR}:.*LISTEN *\([0-9]*\)/.*#\1#p")
   12.43 +  if [ "$PID" != "" ]; then
   12.44 +    kill -9 $PID
   12.45 +  fi
   12.46 +}
   12.47 +
   12.48 +function show_socket_status () {
   12.49 +  netstat -latp 2>/dev/null | grep ":$1 "
   12.50 +}
   12.51 +
   12.52 +## process command line
   12.53 +
   12.54 +case "$1" in
   12.55 +  start|stop|status)
   12.56 +    COMMAND="$1"
   12.57 +    ;;
   12.58 +  *)
   12.59 +    usage
   12.60 +    ;;
   12.61 +esac
   12.62 +
   12.63 +shift
   12.64 +
   12.65 +# options
   12.66 +
   12.67 +NO_OPTS=true
   12.68 +LOGFILE=false
   12.69 +
   12.70 +while getopts "lc:" OPT
   12.71 +do
   12.72 +  NO_OPTS=""
   12.73 +  case "$OPT" in
   12.74 +    l)
   12.75 +      LOGFILE=true
   12.76 +      ;;
   12.77 +    c)
   12.78 +      USER_CONFIG="$OPTARG"
   12.79 +      ;;
   12.80 +    \?)
   12.81 +      usage
   12.82 +      ;;
   12.83 +  esac
   12.84 +done
   12.85 +
   12.86 +shift $(($OPTIND - 1))
   12.87 +
   12.88 +# args
   12.89 +
   12.90 +INPUT=""
   12.91 +
   12.92 +if [ "$#" -ge 1 ]; then
   12.93 +  INPUT="$1"
   12.94 +  shift
   12.95 +fi
   12.96 +
   12.97 +[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
   12.98 +
   12.99 +[ -x "$LIGHTTPD" ] || fail "lighttpd not found at $LIGHTTPD"
  12.100 +
  12.101 +if [ -n "$USER_CONFIG" ]; then
  12.102 +  WWWCONFIG="$USER_CONFIG"
  12.103 +else
  12.104 +  TMP=$(mktemp "/tmp/lighttpd.conf.$$.XXX")
  12.105 +  echo "server.document-root = \"$WWWFINDDIR/www\"" > "$TMP"
  12.106 +  cat "$WWWCONFIG" >> "$TMP"
  12.107 +  WWWCONFIG="$TMP"
  12.108 +fi
  12.109 +
  12.110 +
  12.111 +## main
  12.112 +
  12.113 +WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
  12.114 +SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
  12.115 +MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
  12.116 +
  12.117 +case "$COMMAND" in
  12.118 +  start)
  12.119 +    "$LIGHTTPD" -f "$WWWCONFIG"
  12.120 +    if [ "$LOGFILE" = true ]; then
  12.121 +      (cd "$WWWFINDDIR"; \
  12.122 +       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" "$INPUT") &
  12.123 +    else
  12.124 +      (cd "$WWWFINDDIR"; \
  12.125 +       nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" \
  12.126 +         "$INPUT" > /dev/null 2> /dev/null) &
  12.127 +    fi
  12.128 +    ;;
  12.129 +  stop)
  12.130 +    kill_by_port $SCGIPORT
  12.131 +    kill_by_port $WWWPORT
  12.132 +    ;;
  12.133 +  status)
  12.134 +    show_socket_status $WWWPORT
  12.135 +    show_socket_status $SCGIPORT
  12.136 +    ;;
  12.137 +esac
  12.138 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/WWW_Find/lighttpd.conf	Fri Nov 20 18:36:44 2009 +1100
    13.3 @@ -0,0 +1,20 @@
    13.4 +server.port = 8000
    13.5 +
    13.6 +# debug.log-request-header = "enable"
    13.7 +# debug.log-file-not-found = "enable"
    13.8 +# debug.log-request-handling = "enable"
    13.9 +# debug.log-response-header = "enable"
   13.10 +
   13.11 +mimetype.assign = (
   13.12 +  ".html"   => "text/html; charset=UTF-8",
   13.13 +  ".css"    => "text/css; charset=UTF-8",
   13.14 +)
   13.15 +
   13.16 +server.modules = ( "mod_scgi" )
   13.17 +
   13.18 +scgi.server = ("/isabelle" => ((
   13.19 +		      "host" => "127.0.0.1",
   13.20 +		      "port" => 64000,
   13.21 +		      "check-local" => "disable"
   13.22 +		)))
   13.23 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/WWW_Find/mime.ML	Fri Nov 20 18:36:44 2009 +1100
    14.3 @@ -0,0 +1,56 @@
    14.4 +(*  Title:      mime_types.ML
    14.5 +    Author:     Timothy Bourke, NICTA
    14.6 +
    14.7 +Rudimentary support for mime_types.
    14.8 +*)
    14.9 +
   14.10 +signature MIME =
   14.11 +sig
   14.12 +  datatype t = Type of {
   14.13 +      main : string,
   14.14 +      sub : string, 
   14.15 +      params : (string * string) list
   14.16 +    }
   14.17 +
   14.18 +  val plain : t
   14.19 +  val html : t
   14.20 +  
   14.21 +  val parse_type : string -> t option
   14.22 +  val show_type : t -> string
   14.23 +end;
   14.24 +
   14.25 +structure Mime: MIME =
   14.26 +struct
   14.27 +
   14.28 +datatype t = Type of {
   14.29 +    main : string,
   14.30 +    sub : string, 
   14.31 +    params : (string * string) list
   14.32 +  };
   14.33 +
   14.34 +val strip =
   14.35 +  Substring.dropl Char.isSpace
   14.36 +  #> Substring.dropr Char.isSpace;
   14.37 +
   14.38 +val split_fields =
   14.39 +  Substring.splitl (fn c => c <> #"=")
   14.40 +  #> apsnd (Substring.triml 1)
   14.41 +  #> pairself (Substring.string o strip);
   14.42 +
   14.43 +fun show_param (n, v) = concat ["; ", n, "=", v];
   14.44 +
   14.45 +fun show_type (Type {main, sub, params}) =
   14.46 +      concat ([main, "/", sub] @ map show_param params);
   14.47 +
   14.48 +fun parse_type s =
   14.49 +  (case Substring.fields (Char.contains "/;") (Substring.full s) of
   14.50 +     t::s::ps => SOME (Type { main = (Substring.string o strip) t,
   14.51 +                              sub = (Substring.string o strip) s,
   14.52 +                              params = map split_fields ps })
   14.53 +   | _ => NONE);
   14.54 +
   14.55 +val plain = the (parse_type "text/plain; charset=utf-8");
   14.56 +val html = the (parse_type "text/html; charset=utf-8");
   14.57 +
   14.58 +end;
   14.59 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Tools/WWW_Find/scgi_req.ML	Fri Nov 20 18:36:44 2009 +1100
    15.3 @@ -0,0 +1,160 @@
    15.4 +(*  Title:      parse_scgi_req.ML
    15.5 +    Author:     Timothy Bourke, NICTA
    15.6 +
    15.7 +Parses an SCGI (Simple Common Gateway Interface) header.
    15.8 +See: http://python.ca/scgi/protocol.txt
    15.9 +*)
   15.10 +
   15.11 +signature SCGI_REQ =
   15.12 +sig
   15.13 +  exception InvalidReq of string
   15.14 +
   15.15 +  datatype req_method = Get | Head | Post
   15.16 +
   15.17 +  datatype t = Req of {
   15.18 +      path_info : string,
   15.19 +      path_translated : string,
   15.20 +      script_name : string,
   15.21 +      request_method : req_method,
   15.22 +      query_string : string Symtab.table,
   15.23 +      content_type : Mime.t option,
   15.24 +      environment : Word8VectorSlice.slice Symtab.table
   15.25 +    }
   15.26 +
   15.27 +  val parse : BinIO.instream ->  t * (BinIO.instream * int)
   15.28 +  val test : string -> unit
   15.29 +
   15.30 +  val show : t -> string
   15.31 +end;
   15.32 +
   15.33 +structure ScgiReq : SCGI_REQ =
   15.34 +struct
   15.35 +
   15.36 +exception InvalidReq of string;
   15.37 +
   15.38 +datatype req_method = Get | Head | Post;
   15.39 +
   15.40 +datatype t = Req of {
   15.41 +    path_info : string,
   15.42 +    path_translated : string,
   15.43 +    script_name : string,
   15.44 +    request_method : req_method,
   15.45 +    query_string : string Symtab.table,
   15.46 +    content_type : Mime.t option,
   15.47 +    environment : Word8VectorSlice.slice Symtab.table
   15.48 +  };
   15.49 +
   15.50 +fun parse_req_method "POST" = Post
   15.51 +  | parse_req_method "HEAD" = Head
   15.52 +  | parse_req_method _ = Get;
   15.53 +
   15.54 +fun show_req_method Get = "Get"
   15.55 +  | show_req_method Post = "Post"
   15.56 +  | show_req_method Head = "Head";
   15.57 +
   15.58 +fun find_nulls (idx, 0wx00, idxs) = idx::idxs
   15.59 +  | find_nulls (_, _, idxs) = idxs;
   15.60 +
   15.61 +fun read_net_string fin =
   15.62 +  let
   15.63 +    fun read_size (_, NONE) = raise InvalidReq "Bad netstring length."
   15.64 +      | read_size (t, SOME 0wx3a) = t
   15.65 +      | read_size (t, SOME d) =
   15.66 +          let
   15.67 +            val n = (Word8.toInt d) - 0x30;
   15.68 +          in
   15.69 +            if n >=0 andalso n <= 9
   15.70 +            then read_size (t * 10 + n, BinIO.input1 fin)
   15.71 +            else read_size (t, NONE)
   15.72 +          end;
   15.73 +    val size = read_size (0, BinIO.input1 fin);
   15.74 +    val payload = BinIO.inputN (fin, size);
   15.75 +  in
   15.76 +    (case (Word8Vector.length payload = size, BinIO.input1 fin) of
   15.77 +       (true, SOME 0wx2c) => payload
   15.78 +     | _ => raise InvalidReq "Bad netstring.")
   15.79 +  end;
   15.80 +
   15.81 +fun split_fields vec =
   15.82 +  let
   15.83 +    val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
   15.84 +
   15.85 +    fun pr NONE = "NONE"
   15.86 +      | pr (SOME i) = "SOME " ^ Int.toString i;
   15.87 +
   15.88 +    fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
   15.89 +      | hd_diff _ = NONE;
   15.90 +
   15.91 +    fun slice [] = []
   15.92 +      | slice (idxs as idx::idxs') =
   15.93 +          Word8VectorSlice.slice (vec, idx + 1, hd_diff idxs) :: slice idxs';
   15.94 +
   15.95 +    fun make_pairs (x::y::xys) = (Byte.unpackStringVec x, y) :: make_pairs xys
   15.96 +      | make_pairs _ = [];
   15.97 +
   15.98 +  in make_pairs (slice nulls) end;
   15.99 +
  15.100 +fun parse fin =
  15.101 +  let
  15.102 +    val raw_fields = read_net_string fin;
  15.103 +    val fields = split_fields raw_fields;
  15.104 +    val env = Symtab.make fields;
  15.105 +
  15.106 +    fun field name =
  15.107 +      (case Symtab.lookup env name of
  15.108 +         NONE => ""
  15.109 +       | SOME wv => Byte.unpackStringVec wv);
  15.110 +
  15.111 +    val content_length =
  15.112 +      (the o Int.fromString o field) "CONTENT_LENGTH"
  15.113 +      handle _ => raise InvalidReq "Bad CONTENT_LENGTH";
  15.114 +
  15.115 +    val req = Req {
  15.116 +        path_info = field "PATH_INFO",
  15.117 +        path_translated = field "PATH_TRANSLATED",
  15.118 +        script_name = field "SCRIPT_NAME",
  15.119 +        request_method = (parse_req_method o field) "REQUEST_METHOD",
  15.120 +        query_string = (HttpUtil.parse_query_string o field) "QUERY_STRING",
  15.121 +        content_type = (Mime.parse_type o field) "CONTENT_TYPE",
  15.122 +        environment = env
  15.123 +      }
  15.124 +
  15.125 +   in (req, (fin, content_length)) end; 
  15.126 +
  15.127 +fun show (Req {path_info, path_translated, script_name,
  15.128 +               request_method, query_string, content_type, environment}) =
  15.129 +  let
  15.130 +    fun show_symtab to_string table = let
  15.131 +        fun show (n, v) r = ["\t", n, " = \"", to_string v, "\"\n"] @ r;
  15.132 +      in Symtab.fold show table [] end;
  15.133 +  in
  15.134 +    concat
  15.135 +      (["path_info: \"", path_info, "\"\n",
  15.136 +        "path_translated: \"", path_translated, "\"\n",
  15.137 +        "script_name: \"", script_name, "\"\n",
  15.138 +        "request_method: \"", show_req_method request_method, "\"\n",
  15.139 +        "query_string:\n"]
  15.140 +       @
  15.141 +       show_symtab I query_string
  15.142 +       @
  15.143 +       ["content_type: ",
  15.144 +          (the_default "" o Option.map Mime.show_type) content_type, "\n",
  15.145 +        "environment:\n"]
  15.146 +       @
  15.147 +       show_symtab Byte.unpackStringVec environment)
  15.148 +  end;
  15.149 +
  15.150 +fun test path =
  15.151 +  let
  15.152 +    val fin = BinIO.openIn path;
  15.153 +    val (req, cs) = parse fin;
  15.154 +    val () = TextIO.print (show req);
  15.155 +    val () =
  15.156 +      BinIO.inputN cs
  15.157 +      |> Word8VectorSlice.full
  15.158 +      |> Byte.unpackStringVec
  15.159 +      |> TextIO.print;
  15.160 +  in BinIO.closeIn fin end;
  15.161 +
  15.162 +end;
  15.163 +
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Fri Nov 20 18:36:44 2009 +1100
    16.3 @@ -0,0 +1,125 @@
    16.4 +(*  Title:      scgi_echo.ML
    16.5 +    Author:     Timothy Bourke, NICTA
    16.6 +
    16.7 +Simple SCGI server.
    16.8 +*)
    16.9 +
   16.10 +signature SCGI_SERVER =
   16.11 +sig
   16.12 +  val max_threads : int Unsynchronized.ref
   16.13 +  type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit
   16.14 +  val register : (string * Mime.t option * handler) -> unit
   16.15 +  val server : string -> int -> unit
   16.16 +  val server' : int -> string -> int -> unit (* keeps trying for port *)
   16.17 +end;
   16.18 +
   16.19 +structure ScgiServer : SCGI_SERVER =
   16.20 +struct
   16.21 +val max_threads = Unsynchronized.ref 5;
   16.22 +
   16.23 +type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit;
   16.24 +
   16.25 +local
   16.26 +val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table);
   16.27 +in
   16.28 +fun register (name, mime, f) =
   16.29 +  Unsynchronized.change servers (Symtab.update_new (name, (mime, f)));
   16.30 +fun lookup name = Symtab.lookup (!servers) name;
   16.31 +
   16.32 +fun dump_handlers () = (
   16.33 +    tracing("  with handlers:");
   16.34 +    app (fn (x, _) => tracing ("    - " ^ x)) (Symtab.dest (!servers)))
   16.35 +end;
   16.36 +
   16.37 +fun server server_prefix port =
   16.38 +  let
   16.39 +    val passive_sock = SocketUtil.init_server_socket (SOME "localhost") port;
   16.40 +
   16.41 +    val thread_wait = ConditionVar.conditionVar ();
   16.42 +    val thread_wait_mutex = Mutex.mutex ();
   16.43 +
   16.44 +    local
   16.45 +    val threads = Unsynchronized.ref ([] : Thread.thread list);
   16.46 +    fun purge () = Unsynchronized.change threads (filter Thread.isActive);
   16.47 +    in
   16.48 +    fun add_thread th = Unsynchronized.change threads (cons th);
   16.49 +
   16.50 +    fun launch_thread threadf =
   16.51 +      (purge ();
   16.52 +       if length (!threads) < (!max_threads) then ()
   16.53 +       else (tracing ("Waiting for a free thread...");
   16.54 +             ConditionVar.wait (thread_wait, thread_wait_mutex));
   16.55 +       add_thread
   16.56 +         (Thread.fork
   16.57 +            (fn () => exception_trace threadf,
   16.58 +             [Thread.EnableBroadcastInterrupt true,
   16.59 +              Thread.InterruptState
   16.60 +              Thread.InterruptAsynchOnce])))
   16.61 +    end;
   16.62 +
   16.63 +    fun loop () =
   16.64 +      let
   16.65 +        val (sock, _)= Socket.accept passive_sock;
   16.66 +
   16.67 +        val (sin, sout) = SocketUtil.make_streams sock;
   16.68 +
   16.69 +        fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
   16.70 +        fun send_log msg = (tracing msg; send msg);
   16.71 +
   16.72 +        fun get_content (st, 0) = Word8Vector.fromList []
   16.73 +          | get_content x = BinIO.inputN x;
   16.74 +
   16.75 +        fun do_req () =
   16.76 +          let
   16.77 +            val (req as ScgiReq.Req {path_info, request_method, ...},
   16.78 +                 content_is) =
   16.79 +              ScgiReq.parse sin
   16.80 +              handle ScgiReq.InvalidReq s =>
   16.81 +                (send
   16.82 +                   (HttpUtil.reply_header (HttpStatus.bad_request, NONE, []));
   16.83 +                 raise Fail ("Invalid request: " ^ s));
   16.84 +            val () = tracing ("request: " ^ path_info);
   16.85 +          in
   16.86 +            (case lookup (unprefix server_prefix path_info) of
   16.87 +               NONE => send (HttpUtil.reply_header (HttpStatus.not_found, NONE, []))
   16.88 +             | SOME (NONE, f) => f (req, get_content content_is, send)
   16.89 +             | SOME (t, f) =>
   16.90 +                (send (HttpUtil.reply_header (HttpStatus.ok, t, []));
   16.91 +                 if request_method = ScgiReq.Head then ()
   16.92 +                 else f (req, get_content content_is, send)))
   16.93 +          end;
   16.94 +
   16.95 +        fun thread_req () =
   16.96 +          (do_req () handle e => (warning (exnMessage e));
   16.97 +           BinIO.closeOut sout handle e => warning (exnMessage e);
   16.98 +           BinIO.closeIn sin handle e => warning (exnMessage e);
   16.99 +           Socket.close sock handle e => warning (exnMessage e);
  16.100 +           tracing ("request done.");
  16.101 +           ConditionVar.signal thread_wait);
  16.102 +      in
  16.103 +        launch_thread thread_req;
  16.104 +        loop ()
  16.105 +      end;
  16.106 +  in
  16.107 +    tracing ("SCGI server started.");
  16.108 +    dump_handlers ();
  16.109 +    loop ();
  16.110 +    Socket.close passive_sock
  16.111 +  end;
  16.112 +
  16.113 +local
  16.114 +val delay = 5;
  16.115 +in
  16.116 +fun server' 0 server_prefix port = (warning "Giving up."; exit 1)
  16.117 +  | server' countdown server_prefix port =
  16.118 +      server server_prefix port
  16.119 +        handle OS.SysErr ("bind failed", _) =>
  16.120 +          (warning ("Could not acquire port "
  16.121 +                    ^ Int.toString port ^ ". Trying again in "
  16.122 +                    ^ Int.toString delay ^ " seconds...");
  16.123 +           OS.Process.sleep (Time.fromSeconds delay);
  16.124 +           server' (countdown - 1) server_prefix port);
  16.125 +end;
  16.126 +
  16.127 +end;
  16.128 +
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/WWW_Find/socket_util.ML	Fri Nov 20 18:36:44 2009 +1100
    17.3 @@ -0,0 +1,94 @@
    17.4 +(*  Title:      socket_util.ML
    17.5 +    Author:     Emden R. Gansner and John H. Reppy
    17.6 +                SML Basis Library, section 10
    17.7 +
    17.8 +Routines for working with sockets.
    17.9 +*)
   17.10 +
   17.11 +signature SOCKET_UTIL =
   17.12 +sig
   17.13 +  val init_server_socket : string option -> int ->
   17.14 +                           Socket.passive INetSock.stream_sock
   17.15 +
   17.16 +  val make_streams : Socket.active INetSock.stream_sock
   17.17 +                     -> BinIO.instream * BinIO.outstream
   17.18 +end;
   17.19 +
   17.20 +structure SocketUtil =
   17.21 +struct
   17.22 +
   17.23 +fun init_server_socket hosto port =
   17.24 +  let
   17.25 +    val sock = INetSock.TCP.socket ();
   17.26 +    val addr =
   17.27 +      (case hosto of
   17.28 +         NONE => INetSock.any port
   17.29 +       | SOME host =>
   17.30 +           NetHostDB.getByName host
   17.31 +           |> the
   17.32 +           |> NetHostDB.addr
   17.33 +           |> rpair port
   17.34 +           |> INetSock.toAddr
   17.35 +           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
   17.36 +  in
   17.37 +    Socket.bind (sock, addr);
   17.38 +    Socket.listen (sock, 5);
   17.39 +    sock
   17.40 +  end;
   17.41 +
   17.42 +fun make_streams sock =
   17.43 +  let
   17.44 +    val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
   17.45 +
   17.46 +    val sock_name =
   17.47 +      String.concat [ NetHostDB.toString haddr, ":", Int.toString port ];
   17.48 +
   17.49 +    val rd =
   17.50 +      BinPrimIO.RD {
   17.51 +        name = sock_name,
   17.52 +        chunkSize = Socket.Ctl.getRCVBUF sock,
   17.53 +        readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
   17.54 +        readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
   17.55 +        readVecNB = NONE,
   17.56 +        readArrNB = NONE,
   17.57 +        block = NONE,
   17.58 +        canInput = NONE,
   17.59 +        avail = fn () => NONE,
   17.60 +        getPos = NONE,
   17.61 +        setPos = NONE,
   17.62 +        endPos = NONE,
   17.63 +        verifyPos = NONE,
   17.64 +        close = fn () => Socket.close sock,
   17.65 +        ioDesc = NONE
   17.66 +      };
   17.67 +
   17.68 +    val wr =
   17.69 +      BinPrimIO.WR {
   17.70 +        name = sock_name,
   17.71 +        chunkSize = Socket.Ctl.getSNDBUF sock,
   17.72 +        writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
   17.73 +        writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
   17.74 +        writeVecNB = NONE,
   17.75 +        writeArrNB = NONE,
   17.76 +        block = NONE,
   17.77 +        canOutput = NONE,
   17.78 +        getPos = NONE,
   17.79 +        setPos = NONE,
   17.80 +        endPos = NONE,
   17.81 +        verifyPos = NONE,
   17.82 +        close = fn () => Socket.close sock,
   17.83 +        ioDesc = NONE
   17.84 +      };
   17.85 +
   17.86 +    val in_strm =
   17.87 +      BinIO.mkInstream (
   17.88 +        BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
   17.89 +
   17.90 +    val out_strm =
   17.91 +      BinIO.mkOutstream (
   17.92 +        BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
   17.93 +
   17.94 +    in (in_strm, out_strm) end;
   17.95 +
   17.96 +end;
   17.97 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Fri Nov 20 18:36:44 2009 +1100
    18.3 @@ -0,0 +1,277 @@
    18.4 +(*  Title:      Pure/Thy/unicode_symbols.ML
    18.5 +    Author:     Timothy Bourke, NICTA
    18.6 +
    18.7 +Parse the etc/symbols file.
    18.8 +*)
    18.9 +
   18.10 +signature UNICODE_SYMBOLS =
   18.11 +sig
   18.12 +val symbol_to_unicode : string -> int option
   18.13 +val abbrev_to_unicode : string -> int option
   18.14 +val unicode_to_symbol : int -> string option
   18.15 +val unicode_to_abbrev : int -> string option
   18.16 +val utf8_to_symbols   : string -> string
   18.17 +val utf8              : int list -> string
   18.18 +end;
   18.19 +
   18.20 +structure UnicodeSymbols (*: UNICODE_SYMBOLS*) =
   18.21 +struct
   18.22 +
   18.23 +local (* Lexer *)
   18.24 +
   18.25 +open Basic_Symbol_Pos
   18.26 +
   18.27 +val keywords =
   18.28 +  Scan.make_lexicon (map Symbol.explode ["code", "font", "abbrev", ":"]);
   18.29 +
   18.30 +datatype token_kind =
   18.31 +  Symbol | AsciiSymbol | Keyword | Name | Code | Space | Comment | EOF;
   18.32 +
   18.33 +datatype token = Token of token_kind * string * Position.range;
   18.34 +
   18.35 +fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
   18.36 +
   18.37 +in
   18.38 +
   18.39 +fun mk_eof pos = Token (EOF, "", (pos, Position.none));
   18.40 +
   18.41 +fun str_of_token (Token (_, s, _)) = s;
   18.42 +
   18.43 +fun pos_of_token (Token (_, _, (pos, _))) = pos;
   18.44 +
   18.45 +fun int_of_code (Token (Code, s, _)) = #value (Lexicon.read_xnum s)
   18.46 +  | int_of_code _ = error "internal error in UnicodeSymbols.int_of_code"
   18.47 +
   18.48 +fun is_proper (Token (Space, _, _)) = false
   18.49 +  | is_proper (Token (Comment, _, _)) = false
   18.50 +  | is_proper _ = true;
   18.51 +
   18.52 +fun is_keyword kw (Token (Keyword, kw', _)) = (kw = kw')
   18.53 +  | is_keyword _ _ = false;
   18.54 +
   18.55 +fun is_ascii_sym (Token (AsciiSymbol, _, _)) = true
   18.56 +  | is_ascii_sym _ = false;
   18.57 +
   18.58 +fun is_hex_code (Token (Code, _, _)) = true
   18.59 +  | is_hex_code _ = false;
   18.60 +
   18.61 +fun is_symbol (Token (Symbol, _, _)) = true
   18.62 +  | is_symbol _ = false;
   18.63 +
   18.64 +fun is_name (Token (Name, _, _)) = true
   18.65 +  | is_name _ = false;
   18.66 +
   18.67 +fun is_eof (Token (EOF, _, _)) = true
   18.68 +  | is_eof _ = false;
   18.69 +
   18.70 +fun end_position_of (Token (_, _, (_, epos))) = epos;
   18.71 +
   18.72 +val is_space = symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
   18.73 +val scan_space =
   18.74 +  (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
   18.75 +   ||
   18.76 +   Scan.many is_space @@@ ($$$ "\n")) >> token Space;
   18.77 +
   18.78 +val scan_code = Lexicon.scan_hex #>> token Code;
   18.79 +
   18.80 +val scan_ascii_symbol = Scan.one
   18.81 +  ((fn x => Symbol.is_ascii x andalso
   18.82 +      not (Symbol.is_ascii_letter x
   18.83 +           orelse Symbol.is_ascii_digit x
   18.84 +           orelse Symbol.is_ascii_blank x)) o symbol)
   18.85 +  -- Scan.many (not o Symbol.is_ascii_blank o symbol)
   18.86 +  >> (token AsciiSymbol o op ::);
   18.87 +
   18.88 +fun not_contains xs c = not ((symbol c) mem_string (explode xs));
   18.89 +val scan_comment =
   18.90 +  $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   18.91 +  >> token Comment;
   18.92 +
   18.93 +fun tokenize syms =
   18.94 +  let
   18.95 +    val scanner =
   18.96 +      Scan.one (Symbol.is_symbolic o symbol) >> (token Symbol o single) ||
   18.97 +      scan_comment ||
   18.98 +      scan_space ||
   18.99 +      scan_code ||
  18.100 +      Scan.literal keywords >> token Keyword ||
  18.101 +      scan_ascii_symbol ||
  18.102 +      Lexicon.scan_id >> token Name;
  18.103 +    val scan_token = Symbol_Pos.!!! "Lexical error" (Scan.bulk scanner);
  18.104 +  in
  18.105 +    (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
  18.106 +      (toks, []) => toks
  18.107 +    | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss
  18.108 +                        ^ Position.str_of (#1 (Symbol_Pos.range ss))))
  18.109 +  end;
  18.110 +
  18.111 +val stopper =
  18.112 +  Scan.stopper
  18.113 +    (fn [] => mk_eof Position.none
  18.114 +      | toks => mk_eof (end_position_of (List.last toks))) is_eof;
  18.115 +
  18.116 +end;
  18.117 +
  18.118 +local (* Parser *)
  18.119 +
  18.120 +structure P = OuterParse;
  18.121 +
  18.122 +fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
  18.123 +val hex_code = Scan.one is_hex_code >> int_of_code;
  18.124 +val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
  18.125 +val symbol = Scan.one is_symbol >> (fn t => (str_of_token t, pos_of_token t));
  18.126 +val name = Scan.one is_name >> str_of_token;
  18.127 +
  18.128 +val unicode = $$$ "code" -- $$$ ":" |-- hex_code;
  18.129 +val font = Scan.option ($$$ "font" -- $$$ ":" |-- name);
  18.130 +val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
  18.131 +                        |-- (ascii_sym || $$$ ":" || name));
  18.132 +
  18.133 +in
  18.134 +
  18.135 +val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
  18.136 +
  18.137 +val symbols_path =
  18.138 +  [getenv "ISABELLE_HOME", "etc", "symbols"]
  18.139 +  |> map Path.explode
  18.140 +  |> Path.appends;
  18.141 +
  18.142 +end;
  18.143 +
  18.144 +local (* build tables *)
  18.145 +
  18.146 +fun add_entries ((fromsym, fromabbr, tosym, toabbr), ((sym, pos), uni, oabbr)) =
  18.147 +  (case oabbr of
  18.148 +     NONE =>
  18.149 +       (Symtab.update_new (sym, uni) fromsym,
  18.150 +        fromabbr,
  18.151 +        Inttab.update (uni, sym) tosym,
  18.152 +        toabbr)
  18.153 +   | SOME abbr =>
  18.154 +       (Symtab.update_new (sym, uni) fromsym,
  18.155 +        Symtab.update_new (abbr, uni) fromabbr,
  18.156 +        Inttab.update (uni, sym) tosym,
  18.157 +        Inttab.update (uni, abbr) toabbr))
  18.158 +  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos)
  18.159 +       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos);
  18.160 +
  18.161 +in
  18.162 +
  18.163 +fun read_symbols path =
  18.164 +  let
  18.165 +    val parsed_lines =
  18.166 +      File.read path
  18.167 +      |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
  18.168 +      |> tokenize
  18.169 +      |> filter is_proper
  18.170 +      |> Scan.finite stopper (Scan.repeat line)
  18.171 +      |> fst;
  18.172 +  in
  18.173 +    Library.foldl add_entries
  18.174 +      ((Symtab.empty, Symtab.empty, Inttab.empty, Inttab.empty),
  18.175 +       parsed_lines)
  18.176 +  end;
  18.177 +
  18.178 +end;
  18.179 +
  18.180 +local
  18.181 +val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
  18.182 +in
  18.183 +val symbol_to_unicode = Symtab.lookup fromsym;
  18.184 +val abbrev_to_unicode = Symtab.lookup fromabbr;
  18.185 +val unicode_to_symbol = Inttab.lookup tosym;
  18.186 +val unicode_to_abbrev = Inttab.lookup toabbr;
  18.187 +end;
  18.188 +
  18.189 +fun utf8_to_symbols utf8str =
  18.190 +  let
  18.191 +    val get_next =
  18.192 +      Substring.getc
  18.193 +      #> Option.map (apfst Byte.charToByte);
  18.194 +    val wstr = String.str o Byte.byteToChar;
  18.195 +    val replacement_char = "\<questiondown>";
  18.196 +
  18.197 +    fun word_to_symbol w =
  18.198 +      (case (unicode_to_symbol o Word32.toInt) w of
  18.199 +         NONE => "?"
  18.200 +       | SOME s => s);
  18.201 +
  18.202 +    fun andb32 (w1, w2) =
  18.203 +      Word8.andb(w1, w2)
  18.204 +      |> Word8.toLarge
  18.205 +      |> Word32.fromLarge;
  18.206 +
  18.207 +    fun read_next (ss, 0, c) = (word_to_symbol c, ss)
  18.208 +      | read_next (ss, n, c) =
  18.209 +          (case get_next ss of
  18.210 +             NONE => (replacement_char, ss)
  18.211 +           | SOME (w, ss') =>
  18.212 +               if Word8.andb (w, 0wxc0) <> 0wx80
  18.213 +               then (replacement_char, ss')
  18.214 +               else
  18.215 +                 let
  18.216 +                   val w' = (Word8.andb (w, 0wx3f));
  18.217 +                   val bw = (Word32.fromLarge o Word8.toLarge) w';
  18.218 +                   val c' = Word32.<< (c, 0wx6);
  18.219 +                 in read_next (ss', n - 1, Word32.orb (c', bw)) end);
  18.220 +
  18.221 +    fun do_char (w, ss) =
  18.222 +      if Word8.andb (w, 0wx80) = 0wx00
  18.223 +      then (wstr w, ss)
  18.224 +      else if Word8.andb (w, 0wx60) = 0wx40
  18.225 +      then read_next (ss, 1, andb32 (w, 0wx1f))
  18.226 +      else if Word8.andb (w, 0wxf0) = 0wxe0
  18.227 +      then read_next (ss, 2, andb32 (w, 0wx0f))
  18.228 +      else if Word8.andb (w, 0wxf8) = 0wxf0
  18.229 +      then read_next (ss, 3, andb32 (w, 0wx07))
  18.230 +      else (replacement_char, ss);
  18.231 +
  18.232 +    fun read (rs, ss) =
  18.233 +      (case Option.map do_char (get_next ss) of
  18.234 +         NONE => (implode o rev) rs
  18.235 +       | SOME (s, ss') => read (s::rs, ss'));
  18.236 +  in read ([], Substring.full utf8str) end;
  18.237 +
  18.238 +local
  18.239 +
  18.240 +fun consec n =
  18.241 +  fn w => (
  18.242 +    Word32.>> (w, Word.fromInt (n * 6))
  18.243 +    |> (curry Word32.andb) 0wx3f
  18.244 +    |> (curry Word32.orb) 0wx80
  18.245 +    |> Word8.fromLargeWord o Word32.toLargeWord);
  18.246 +
  18.247 +fun stamp n =
  18.248 +  fn w => (
  18.249 +    Word32.>> (w, Word.fromInt (n * 6))
  18.250 +    |> (curry Word32.andb) (Word32.>> (0wx000000ff, Word.fromInt (n + 2)))
  18.251 +    |> (curry Word32.orb) (Word32.<< (0wxffffffff, Word.fromInt (7 - n)))
  18.252 +    |> Word8.fromLargeWord o Word32.toLargeWord);
  18.253 +
  18.254 +fun to_utf8_bytes i =
  18.255 +  if i <= 0x007f
  18.256 +  then [Word8.fromInt i]
  18.257 +  else let
  18.258 +    val w = Word32.fromInt i;
  18.259 +  in
  18.260 +    if i < 0x07ff
  18.261 +    then [stamp 1 w, consec 0 w]
  18.262 +    else if i < 0xffff
  18.263 +    then [stamp 2 w, consec 1 w, consec 0 w]
  18.264 +    else if i < 0x10ffff
  18.265 +    then [stamp 3 w, consec 2 w, consec 1 w, consec 0 w]
  18.266 +    else []
  18.267 +  end;
  18.268 +
  18.269 +in
  18.270 +
  18.271 +fun utf8 is =
  18.272 +  map to_utf8_bytes is
  18.273 +  |> flat
  18.274 +  |> Word8Vector.fromList
  18.275 +  |> Byte.bytesToString;
  18.276 +
  18.277 +end
  18.278 +
  18.279 +end;
  18.280 +
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/WWW_Find/www/basic.css	Fri Nov 20 18:36:44 2009 +1100
    19.3 @@ -0,0 +1,109 @@
    19.4 +
    19.5 +body {
    19.6 +    font-family: sans-serif;
    19.7 +    background-color: white;
    19.8 +}
    19.9 +
   19.10 +p.error {
   19.11 +    font-weight: bold;
   19.12 +    color: #ff0000;
   19.13 +}
   19.14 +
   19.15 +p.info {
   19.16 +    font-style: italic;
   19.17 +}
   19.18 +
   19.19 +input#query {
   19.20 +    width: 100%;
   19.21 +}
   19.22 +
   19.23 +legend {
   19.24 +    padding : 0.5em;
   19.25 +    font-weight: bold;
   19.26 +}
   19.27 +
   19.28 +label {
   19.29 +    width: 8em;
   19.30 +    float: left;
   19.31 +}
   19.32 +
   19.33 +fieldset {
   19.34 +    padding: 0 1em 1em 1em;
   19.35 +}
   19.36 +
   19.37 +div.settings {
   19.38 +    padding-top: 2em;
   19.39 +    float: left;
   19.40 +}
   19.41 +
   19.42 +div.settings label {
   19.43 +    font-style: italic;
   19.44 +}
   19.45 +
   19.46 +div.settings div {
   19.47 +    padding-top: 1ex;
   19.48 +}
   19.49 +
   19.50 +div.mainbuttons {
   19.51 +    margin-top: 8.5ex;
   19.52 +    float: right
   19.53 +}
   19.54 +
   19.55 +div.mainbuttons #reset {
   19.56 +    margin-right: 5em;
   19.57 +}
   19.58 +
   19.59 +table.findtheorems {
   19.60 +    width: 100%;
   19.61 +    padding-top: 1em;
   19.62 +    padding-bottom: 2em;
   19.63 +}
   19.64 +
   19.65 +table.findtheorems tr.row0 { background-color: white; }
   19.66 +table.findtheorems tr.row1 { background-color: #f5f5f5; }
   19.67 +table.findtheorems tbody tr:hover { background-color: #dcdcdc; }
   19.68 +
   19.69 +table.findtheorems td {
   19.70 +    vertical-align: top;
   19.71 +    padding-left: 1em;
   19.72 +    padding-bottom: 1em;
   19.73 +}
   19.74 +
   19.75 +table.findtheorems td.name {
   19.76 +    font-size: small;
   19.77 +    font-style: italic;
   19.78 +    padding-right: 1em;
   19.79 +}
   19.80 +table.findtheorems td.thm {
   19.81 +    vertical-align: top;
   19.82 +    font-size: small;
   19.83 +}
   19.84 +table.findtheorems td.thm pre {
   19.85 +    margin: 0em;
   19.86 +}
   19.87 +table.findtheorems th {
   19.88 +    text-align: left;
   19.89 +    padding-bottom: 1ex;
   19.90 +}
   19.91 +
   19.92 +table.findtheoremsquery th {
   19.93 +    font-weight: normal;
   19.94 +    text-align: left;
   19.95 +    padding-top: 1em;
   19.96 +}
   19.97 +
   19.98 +span.class { color: #ff0000 }
   19.99 +span.tfree { color: #9370d8 }
  19.100 +span.tvar { color: #9370d8 }
  19.101 +span.free { color: #add8e6 }
  19.102 +span.bound { color: #008400 }
  19.103 +span.var { color: #00008b }
  19.104 +span.xstr { color: #000000 }
  19.105 +
  19.106 +span.sorried:after { content: " [!]"; }
  19.107 +
  19.108 +div.help a {
  19.109 +    font-size: xx-small;
  19.110 +    color: #d3d3d3;
  19.111 +}
  19.112 +
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Tools/WWW_Find/www/find_theorems.js	Fri Nov 20 18:36:44 2009 +1100
    20.3 @@ -0,0 +1,410 @@
    20.4 +/* $Id$
    20.5 + * Author: Timothy Bourke, NICTA
    20.6 + */
    20.7 +var utf8 = new Object();
    20.8 +utf8['\\<supseteq>'] = 'โŠ‡';
    20.9 +utf8['\\<KK>'] = '๐”Ž';
   20.10 +utf8['\\<up>'] = 'โ†‘';
   20.11 +utf8['\\<otimes>'] = 'โŠ—';
   20.12 +utf8['\\<aa>'] = '๐”ž';
   20.13 +utf8['\\<dagger>'] = 'โ€ ';
   20.14 +utf8['\\<frown>'] = 'โŒข';
   20.15 +utf8['\\<guillemotleft>'] = 'ยซ';
   20.16 +utf8['\\<qq>'] = '๐”ฎ';
   20.17 +utf8['\\<X>'] = '๐’ณ';
   20.18 +utf8['\\<triangleright>'] = 'โ–น';
   20.19 +utf8['\\<guillemotright>'] = 'ยป';
   20.20 +utf8['\\<nu>'] = 'ฮฝ';
   20.21 +utf8['\\<sim>'] = 'โˆผ';
   20.22 +utf8['\\<rightharpoondown>'] = 'โ‡';
   20.23 +utf8['\\<p>'] = '๐—‰';
   20.24 +utf8['\\<Up>'] = 'โ‡‘';
   20.25 +utf8['\\<triangleq>'] = 'โ‰œ';
   20.26 +utf8['\\<nine>'] = '๐Ÿต';
   20.27 +utf8['\\<preceq>'] = 'โ‰ผ';
   20.28 +utf8['\\<nabla>'] = 'โˆ‡';
   20.29 +utf8['\\<FF>'] = '๐”‰';
   20.30 +utf8['\\<Im>'] = 'โ„‘';
   20.31 +utf8['\\<VV>'] = '๐”™';
   20.32 +utf8['\\<spacespace>'] = 'โฃ';
   20.33 +utf8['\\<and>'] = 'โˆง';
   20.34 +utf8['\\<mapsto>'] = 'โ†ฆ';
   20.35 +utf8['\\<ll>'] = '๐”ฉ';
   20.36 +utf8['\\<F>'] = 'โ„ฑ';
   20.37 +utf8['\\<degree>'] = 'ยฐ';
   20.38 +utf8['\\<beta>'] = 'ฮฒ';
   20.39 +utf8['\\<Colon>'] = 'โˆท';
   20.40 +utf8['\\<bool>'] = '๐”น';
   20.41 +utf8['\\<e>'] = '๐–พ';
   20.42 +utf8['\\<lozenge>'] = 'โ—Š';
   20.43 +utf8['\\<u>'] = '๐—Ž';
   20.44 +utf8['\\<sharp>'] = 'โ™ฏ';
   20.45 +utf8['\\<Longleftrightarrow>'] = 'โŸบ';
   20.46 +utf8['\\<Otimes>'] = 'โจ‚';
   20.47 +utf8['\\<EE>'] = '๐”ˆ';
   20.48 +utf8['\\<I>'] = 'โ„';
   20.49 +utf8['\\<UU>'] = '๐”˜';
   20.50 +utf8['\\<exclamdown>'] = 'ยก';
   20.51 +utf8['\\<dots>'] = 'โ€ฆ';
   20.52 +utf8['\\<N>'] = '๐’ฉ';
   20.53 +utf8['\\<kk>'] = '๐”จ';
   20.54 +utf8['\\<plusminus>'] = 'ยฑ';
   20.55 +utf8['\\<E>'] = 'โ„ฐ';
   20.56 +utf8['\\<triangle>'] = 'โ–ณ';
   20.57 +utf8['\\<eta>'] = 'ฮท';
   20.58 +utf8['\\<triangleleft>'] = 'โ—ƒ';
   20.59 +utf8['\\<chi>'] = 'ฯ‡';
   20.60 +utf8['\\<z>'] = '๐—“';
   20.61 +utf8['\\<hungarumlaut>'] = 'ห';
   20.62 +utf8['\\<partial>'] = 'โˆ‚';
   20.63 +utf8['\\<three>'] = '๐Ÿฏ';
   20.64 +utf8['\\<lesssim>'] = 'โ‰ฒ';
   20.65 +utf8['\\<subset>'] = 'โŠ‚';
   20.66 +utf8['\\<H>'] = 'โ„‹';
   20.67 +utf8['\\<leftarrow>'] = 'โ†';
   20.68 +utf8['\\<PP>'] = '๐”“';
   20.69 +utf8['\\<sqsupseteq>'] = 'โŠ’';
   20.70 +utf8['\\<R>'] = 'โ„›';
   20.71 +utf8['\\<bowtie>'] = 'โจ';
   20.72 +utf8['\\<C>'] = '๐’ž';
   20.73 +utf8['\\<ddagger>'] = 'โ€ก';
   20.74 +utf8['\\<ff>'] = '๐”ฃ';
   20.75 +utf8['\\<turnstile>'] = 'โŠข';
   20.76 +utf8['\\<bar>'] = 'ยฆ';
   20.77 +utf8['\\<propto>'] = 'โˆ';
   20.78 +utf8['\\<S>'] = '๐’ฎ';
   20.79 +utf8['\\<vv>'] = '๐”ณ';
   20.80 +utf8['\\<lhd>'] = 'โŠฒ';
   20.81 +utf8['\\<paragraph>'] = 'ยถ';
   20.82 +utf8['\\<mu>'] = 'ฮผ';
   20.83 +utf8['\\<rightharpoonup>'] = 'โ‡€';
   20.84 +utf8['\\<Inter>'] = 'โ‹‚';
   20.85 +utf8['\\<o>'] = '๐—ˆ';
   20.86 +utf8['\\<asymp>'] = 'โ‰';
   20.87 +utf8['\\<Leftarrow>'] = 'โ‡';
   20.88 +utf8['\\<Sqinter>'] = 'โจ…';
   20.89 +utf8['\\<eight>'] = '๐Ÿด';
   20.90 +utf8['\\<succeq>'] = 'โ‰ฝ';
   20.91 +utf8['\\<forall>'] = 'โˆ€';
   20.92 +utf8['\\<complex>'] = 'โ„‚';
   20.93 +utf8['\\<GG>'] = '๐”Š';
   20.94 +utf8['\\<Coprod>'] = 'โˆ';
   20.95 +utf8['\\<L>'] = 'โ„’';
   20.96 +utf8['\\<WW>'] = '๐”š';
   20.97 +utf8['\\<leadsto>'] = 'โ†';
   20.98 +utf8['\\<D>'] = '๐’Ÿ';
   20.99 +utf8['\\<angle>'] = 'โˆ ';
  20.100 +utf8['\\<section>'] = 'ยง';
  20.101 +utf8['\\<TTurnstile>'] = 'โŠซ';
  20.102 +utf8['\\<mm>'] = '๐”ช';
  20.103 +utf8['\\<T>'] = '๐’ฏ';
  20.104 +utf8['\\<alpha>'] = 'ฮฑ';
  20.105 +utf8['\\<leftharpoondown>'] = 'โ†ฝ';
  20.106 +utf8['\\<rho>'] = 'ฯ';
  20.107 +utf8['\\<wrong>'] = 'โ‰€';
  20.108 +utf8['\\<l>'] = '๐—…';
  20.109 +utf8['\\<doteq>'] = 'โ‰';
  20.110 +utf8['\\<times>'] = 'ร—';
  20.111 +utf8['\\<noteq>'] = 'โ‰ ';
  20.112 +utf8['\\<rangle>'] = 'โŸฉ';
  20.113 +utf8['\\<div>'] = 'รท';
  20.114 +utf8['\\<Longrightarrow>'] = 'โŸน';
  20.115 +utf8['\\<BB>'] = '๐”…';
  20.116 +utf8['\\<sqsupset>'] = 'โŠ';
  20.117 +utf8['\\<rightarrow>'] = 'โ†’';
  20.118 +utf8['\\<real>'] = 'โ„';
  20.119 +utf8['\\<hh>'] = '๐”ฅ';
  20.120 +utf8['\\<Phi>'] = 'ฮฆ';
  20.121 +utf8['\\<integral>'] = 'โˆซ';
  20.122 +utf8['\\<CC>'] = 'โ„ญ';
  20.123 +utf8['\\<euro>'] = 'โ‚ฌ';
  20.124 +utf8['\\<xx>'] = '๐”ต';
  20.125 +utf8['\\<Y>'] = '๐’ด';
  20.126 +utf8['\\<zeta>'] = 'ฮถ';
  20.127 +utf8['\\<longleftarrow>'] = 'โŸต';
  20.128 +utf8['\\<a>'] = '๐–บ';
  20.129 +utf8['\\<onequarter>'] = 'ยผ';
  20.130 +utf8['\\<And>'] = 'โ‹€';
  20.131 +utf8['\\<downharpoonright>'] = 'โ‡‚';
  20.132 +utf8['\\<phi>'] = 'ฯ†';
  20.133 +utf8['\\<q>'] = '๐—Š';
  20.134 +utf8['\\<Rightarrow>'] = 'โ‡’';
  20.135 +utf8['\\<clubsuit>'] = 'โ™ฃ';
  20.136 +utf8['\\<ggreater>'] = 'โ‰ซ';
  20.137 +utf8['\\<two>'] = '๐Ÿฎ';
  20.138 +utf8['\\<succ>'] = 'โ‰ป';
  20.139 +utf8['\\<AA>'] = '๐”„';
  20.140 +utf8['\\<lparr>'] = 'โฆ‡';
  20.141 +utf8['\\<Squnion>'] = 'โจ†';
  20.142 +utf8['\\<HH>'] = 'โ„Œ';
  20.143 +utf8['\\<sqsubseteq>'] = 'โŠ‘';
  20.144 +utf8['\\<QQ>'] = '๐””';
  20.145 +utf8['\\<setminus>'] = 'โˆ–';
  20.146 +utf8['\\<Lambda>'] = 'ฮ›';
  20.147 +utf8['\\<Re>'] = 'โ„œ';
  20.148 +utf8['\\<J>'] = '๐’ฅ';
  20.149 +utf8['\\<gg>'] = '๐”ค';
  20.150 +utf8['\\<hyphen>'] = 'ยญ';
  20.151 +utf8['\\<B>'] = 'โ„ฌ';
  20.152 +utf8['\\<Z>'] = '๐’ต';
  20.153 +utf8['\\<ww>'] = '๐”ด';
  20.154 +utf8['\\<lambda>'] = 'ฮป';
  20.155 +utf8['\\<onehalf>'] = 'ยฝ';
  20.156 +utf8['\\<f>'] = '๐–ฟ';
  20.157 +utf8['\\<Or>'] = 'โ‹';
  20.158 +utf8['\\<v>'] = '๐—';
  20.159 +utf8['\\<natural>'] = 'โ™ฎ';
  20.160 +utf8['\\<seven>'] = '๐Ÿณ';
  20.161 +utf8['\\<Oplus>'] = 'โจ';
  20.162 +utf8['\\<subseteq>'] = 'โŠ†';
  20.163 +utf8['\\<rfloor>'] = 'โŒ‹';
  20.164 +utf8['\\<LL>'] = '๐”';
  20.165 +utf8['\\<Sum>'] = 'โˆ‘';
  20.166 +utf8['\\<ominus>'] = 'โŠ–';
  20.167 +utf8['\\<bb>'] = '๐”Ÿ';
  20.168 +utf8['\\<Pi>'] = 'ฮ ';
  20.169 +utf8['\\<cent>'] = 'ยข';
  20.170 +utf8['\\<diamond>'] = 'โ—‡';
  20.171 +utf8['\\<mho>'] = 'โ„ง';
  20.172 +utf8['\\<O>'] = '๐’ช';
  20.173 +utf8['\\<rr>'] = '๐”ฏ';
  20.174 +utf8['\\<twosuperior>'] = 'ยฒ';
  20.175 +utf8['\\<leftharpoonup>'] = 'โ†ผ';
  20.176 +utf8['\\<pi>'] = 'ฯ€';
  20.177 +utf8['\\<k>'] = '๐—„';
  20.178 +utf8['\\<star>'] = 'โ‹†';
  20.179 +utf8['\\<rightleftharpoons>'] = 'โ‡Œ';
  20.180 +utf8['\\<equiv>'] = 'โ‰ก';
  20.181 +utf8['\\<langle>'] = 'โŸจ';
  20.182 +utf8['\\<Longleftarrow>'] = 'โŸธ';
  20.183 +utf8['\\<nexists>'] = 'โˆ„';
  20.184 +utf8['\\<Odot>'] = 'โจ€';
  20.185 +utf8['\\<lfloor>'] = 'โŒŠ';
  20.186 +utf8['\\<sqsubset>'] = 'โŠ';
  20.187 +utf8['\\<SS>'] = '๐”–';
  20.188 +utf8['\\<box>'] = 'โ–ก';
  20.189 +utf8['\\<index>'] = 'ฤฑ';
  20.190 +utf8['\\<pounds>'] = 'ยฃ';
  20.191 +utf8['\\<Upsilon>'] = 'ฮฅ';
  20.192 +utf8['\\<ii>'] = '๐”ฆ';
  20.193 +utf8['\\<hookleftarrow>'] = 'โ†ฉ';
  20.194 +utf8['\\<P>'] = '๐’ซ';
  20.195 +utf8['\\<threesuperior>'] = 'ยณ';
  20.196 +utf8['\\<epsilon>'] = 'ฮต';
  20.197 +utf8['\\<yy>'] = '๐”ถ';
  20.198 +utf8['\\<h>'] = '๐—';
  20.199 +utf8['\\<upsilon>'] = 'ฯ…';
  20.200 +utf8['\\<x>'] = '๐—‘';
  20.201 +utf8['\\<not>'] = 'ยฌ';
  20.202 +utf8['\\<le>'] = 'โ‰ค';
  20.203 +utf8['\\<one>'] = '๐Ÿญ';
  20.204 +utf8['\\<cdots>'] = 'โ‹ฏ';
  20.205 +utf8['\\<some>'] = 'ฯต';
  20.206 +utf8['\\<Prod>'] = 'โˆ';
  20.207 +utf8['\\<NN>'] = '๐”‘';
  20.208 +utf8['\\<squnion>'] = 'โŠ”';
  20.209 +utf8['\\<dd>'] = '๐”ก';
  20.210 +utf8['\\<top>'] = 'โŠค';
  20.211 +utf8['\\<dieresis>'] = 'ยจ';
  20.212 +utf8['\\<tt>'] = '๐”ฑ';
  20.213 +utf8['\\<U>'] = '๐’ฐ';
  20.214 +utf8['\\<unlhd>'] = 'โŠด';
  20.215 +utf8['\\<cedilla>'] = 'ยธ';
  20.216 +utf8['\\<kappa>'] = 'ฮบ';
  20.217 +utf8['\\<amalg>'] = 'โจฟ';
  20.218 +utf8['\\<restriction>'] = 'โ†พ';
  20.219 +utf8['\\<struct>'] = 'โ‹„';
  20.220 +utf8['\\<m>'] = '๐—†';
  20.221 +utf8['\\<six>'] = '๐Ÿฒ';
  20.222 +utf8['\\<midarrow>'] = 'โ”€';
  20.223 +utf8['\\<lbrace>'] = 'โฆƒ';
  20.224 +utf8['\\<lessapprox>'] = 'โช…';
  20.225 +utf8['\\<MM>'] = '๐”';
  20.226 +utf8['\\<down>'] = 'โ†“';
  20.227 +utf8['\\<oplus>'] = 'โŠ•';
  20.228 +utf8['\\<wp>'] = 'โ„˜';
  20.229 +utf8['\\<surd>'] = 'โˆš';
  20.230 +utf8['\\<cc>'] = '๐” ';
  20.231 +utf8['\\<bottom>'] = 'โŠฅ';
  20.232 +utf8['\\<copyright>'] = 'ยฉ';
  20.233 +utf8['\\<ZZ>'] = 'โ„จ';
  20.234 +utf8['\\<union>'] = 'โˆช';
  20.235 +utf8['\\<V>'] = '๐’ฑ';
  20.236 +utf8['\\<ss>'] = '๐”ฐ';
  20.237 +utf8['\\<unrhd>'] = 'โŠต';
  20.238 +utf8['\\<onesuperior>'] = 'ยน';
  20.239 +utf8['\\<b>'] = '๐–ป';
  20.240 +utf8['\\<downharpoonleft>'] = 'โ‡ƒ';
  20.241 +utf8['\\<cdot>'] = 'โ‹…';
  20.242 +utf8['\\<r>'] = '๐—‹';
  20.243 +utf8['\\<Midarrow>'] = 'โ•';
  20.244 +utf8['\\<Down>'] = 'โ‡“';
  20.245 +utf8['\\<diamondsuit>'] = 'โ™ข';
  20.246 +utf8['\\<rbrakk>'] = 'โŸง';
  20.247 +utf8['\\<lless>'] = 'โ‰ช';
  20.248 +utf8['\\<longleftrightarrow>'] = 'โŸท';
  20.249 +utf8['\\<prec>'] = 'โ‰บ';
  20.250 +utf8['\\<emptyset>'] = 'โˆ…';
  20.251 +utf8['\\<rparr>'] = 'โฆˆ';
  20.252 +utf8['\\<Delta>'] = 'ฮ”';
  20.253 +utf8['\\<XX>'] = '๐”›';
  20.254 +utf8['\\<parallel>'] = 'โˆฅ';
  20.255 +utf8['\\<K>'] = '๐’ฆ';
  20.256 +utf8['\\<nn>'] = '๐”ซ';
  20.257 +utf8['\\<registered>'] = 'ยฎ';
  20.258 +utf8['\\<M>'] = 'โ„ณ';
  20.259 +utf8['\\<delta>'] = 'ฮด';
  20.260 +utf8['\\<threequarters>'] = 'ยพ';
  20.261 +utf8['\\<g>'] = '๐—€';
  20.262 +utf8['\\<cong>'] = 'โ‰…';
  20.263 +utf8['\\<tau>'] = 'ฯ„';
  20.264 +utf8['\\<w>'] = '๐—';
  20.265 +utf8['\\<ge>'] = 'โ‰ฅ';
  20.266 +utf8['\\<flat>'] = 'โ™ญ';
  20.267 +utf8['\\<zero>'] = '๐Ÿฌ';
  20.268 +utf8['\\<Uplus>'] = 'โจ„';
  20.269 +utf8['\\<longmapsto>'] = 'โŸผ';
  20.270 +utf8['\\<supset>'] = 'โŠƒ';
  20.271 +utf8['\\<in>'] = 'โˆˆ';
  20.272 +utf8['\\<sqinter>'] = 'โŠ“';
  20.273 +utf8['\\<OO>'] = '๐”’';
  20.274 +utf8['\\<updown>'] = 'โ†•';
  20.275 +utf8['\\<circ>'] = 'โˆ˜';
  20.276 +utf8['\\<rat>'] = 'โ„š';
  20.277 +utf8['\\<stileturn>'] = 'โŠฃ';
  20.278 +utf8['\\<ee>'] = '๐”ข';
  20.279 +utf8['\\<Omega>'] = 'ฮฉ';
  20.280 +utf8['\\<or>'] = 'โˆจ';
  20.281 +utf8['\\<inverse>'] = 'ยฏ';
  20.282 +utf8['\\<rhd>'] = 'โŠณ';
  20.283 +utf8['\\<uu>'] = '๐”ฒ';
  20.284 +utf8['\\<iota>'] = 'ฮน';
  20.285 +utf8['\\<d>'] = '๐–ฝ';
  20.286 +utf8['\\<questiondown>'] = 'ยฟ';
  20.287 +utf8['\\<Union>'] = 'โ‹ƒ';
  20.288 +utf8['\\<omega>'] = 'ฯ‰';
  20.289 +utf8['\\<approx>'] = 'โ‰ˆ';
  20.290 +utf8['\\<t>'] = '๐—';
  20.291 +utf8['\\<Updown>'] = 'โ‡•';
  20.292 +utf8['\\<spadesuit>'] = 'โ™ ';
  20.293 +utf8['\\<five>'] = '๐Ÿฑ';
  20.294 +utf8['\\<exists>'] = 'โˆƒ';
  20.295 +utf8['\\<rceil>'] = 'โŒ‰';
  20.296 +utf8['\\<JJ>'] = '๐”';
  20.297 +utf8['\\<minusplus>'] = 'โˆ“';
  20.298 +utf8['\\<nat>'] = 'โ„•';
  20.299 +utf8['\\<oslash>'] = 'โŠ˜';
  20.300 +utf8['\\<A>'] = '๐’œ';
  20.301 +utf8['\\<Xi>'] = 'ฮž';
  20.302 +utf8['\\<currency>'] = 'ยค';
  20.303 +utf8['\\<Turnstile>'] = 'โŠจ';
  20.304 +utf8['\\<hookrightarrow>'] = 'โ†ช';
  20.305 +utf8['\\<pp>'] = '๐”ญ';
  20.306 +utf8['\\<Q>'] = '๐’ฌ';
  20.307 +utf8['\\<aleph>'] = 'โ„ต';
  20.308 +utf8['\\<acute>'] = 'ยด';
  20.309 +utf8['\\<xi>'] = 'ฮพ';
  20.310 +utf8['\\<simeq>'] = 'โ‰ƒ';
  20.311 +utf8['\\<i>'] = '๐—‚';
  20.312 +utf8['\\<Join>'] = 'โ‹ˆ';
  20.313 +utf8['\\<y>'] = '๐—’';
  20.314 +utf8['\\<lbrakk>'] = 'โŸฆ';
  20.315 +utf8['\\<greatersim>'] = 'โ‰ณ';
  20.316 +utf8['\\<greaterapprox>'] = 'โช†';
  20.317 +utf8['\\<longrightarrow>'] = 'โŸถ';
  20.318 +utf8['\\<lceil>'] = 'โŒˆ';
  20.319 +utf8['\\<Gamma>'] = 'ฮ“';
  20.320 +utf8['\\<odot>'] = 'โŠ™';
  20.321 +utf8['\\<YY>'] = '๐”œ';
  20.322 +utf8['\\<infinity>'] = 'โˆž';
  20.323 +utf8['\\<Sigma>'] = 'ฮฃ';
  20.324 +utf8['\\<yen>'] = 'ยฅ';
  20.325 +utf8['\\<int>'] = 'โ„ค';
  20.326 +utf8['\\<tturnstile>'] = 'โŠฉ';
  20.327 +utf8['\\<oo>'] = '๐”ฌ';
  20.328 +utf8['\\<ointegral>'] = 'โˆฎ';
  20.329 +utf8['\\<gamma>'] = 'ฮณ';
  20.330 +utf8['\\<upharpoonleft>'] = 'โ†ฟ';
  20.331 +utf8['\\<sigma>'] = 'ฯƒ';
  20.332 +utf8['\\<n>'] = '๐—‡';
  20.333 +utf8['\\<rbrace>'] = 'โฆ„';
  20.334 +utf8['\\<DD>'] = '๐”‡';
  20.335 +utf8['\\<notin>'] = 'โˆ‰';
  20.336 +utf8['\\<j>'] = '๐—ƒ';
  20.337 +utf8['\\<uplus>'] = 'โŠŽ';
  20.338 +utf8['\\<leftrightarrow>'] = 'โ†”';
  20.339 +utf8['\\<TT>'] = '๐”—';
  20.340 +utf8['\\<bullet>'] = 'โˆ™';
  20.341 +utf8['\\<Theta>'] = 'ฮ˜';
  20.342 +utf8['\\<smile>'] = 'โŒฃ';
  20.343 +utf8['\\<G>'] = '๐’ข';
  20.344 +utf8['\\<jj>'] = '๐”ง';
  20.345 +utf8['\\<inter>'] = 'โˆฉ';
  20.346 +utf8['\\<Psi>'] = 'ฮจ';
  20.347 +utf8['\\<ordfeminine>'] = 'ยช';
  20.348 +utf8['\\<W>'] = '๐’ฒ';
  20.349 +utf8['\\<zz>'] = '๐”ท';
  20.350 +utf8['\\<theta>'] = 'ฮธ';
  20.351 +utf8['\\<ordmasculine>'] = 'ยบ';
  20.352 +utf8['\\<c>'] = '๐–ผ';
  20.353 +utf8['\\<psi>'] = 'ฯˆ';
  20.354 +utf8['\\<s>'] = '๐—Œ';
  20.355 +utf8['\\<Leftrightarrow>'] = 'โ‡”';
  20.356 +utf8['\\<heartsuit>'] = 'โ™ก';
  20.357 +utf8['\\<four>'] = '๐Ÿฐ';
  20.358 +
  20.359 +var re_xsymbol = /\\<.*?>/g;
  20.360 +
  20.361 +function encodequery(ele) {
  20.362 +  var text = ele.value;
  20.363 +  var otext = text;
  20.364 +  var pos = getCaret(ele);
  20.365 +
  20.366 +  xsymbols = text.match(re_xsymbol);
  20.367 +  for (i in xsymbols) {
  20.368 +    var repl = utf8[xsymbols[i]];
  20.369 +    if (repl) {
  20.370 +	text = text.replace(xsymbols[i], repl, "g");
  20.371 +    }
  20.372 +  }
  20.373 +
  20.374 +  if (text != otext) {
  20.375 +    ele.value = text;
  20.376 +
  20.377 +    if (pos != -1) {
  20.378 +      pos = pos - (otext.length - text.length);
  20.379 +      setCaret(ele, pos);
  20.380 +    }
  20.381 +  }
  20.382 +}
  20.383 +
  20.384 +/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */
  20.385 +function getCaret(obj) {
  20.386 +  var pos = -1;
  20.387 +
  20.388 +  if (document.selection) { // IE
  20.389 +    obj.focus ();
  20.390 +    var sel = document.selection.createRange();
  20.391 +    var sellen = document.selection.createRange().text.length;
  20.392 +    sel.moveStart ('character', -obj.value.length);
  20.393 +    pos = sel.text.length - sellen;
  20.394 +
  20.395 +  } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko
  20.396 +    pos = obj.selectionStart;
  20.397 +  }
  20.398 +  
  20.399 +  return pos;
  20.400 +}
  20.401 +
  20.402 +/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */
  20.403 +function setCaret(obj, pos) {
  20.404 +  if (obj.createTextRange) {
  20.405 +      var range = obj.createTextRange();
  20.406 +      range.move("character", pos);
  20.407 +      range.select();
  20.408 +  } else if (obj.selectionStart) {
  20.409 +      obj.focus();
  20.410 +      obj.setSelectionRange(pos, pos);
  20.411 +  }
  20.412 +}
  20.413 +
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Tools/WWW_Find/www/pasting_help.html	Fri Nov 20 18:36:44 2009 +1100
    21.3 @@ -0,0 +1,19 @@
    21.4 +<html>
    21.5 +  <head>
    21.6 +    <title>Find Theorems: help pasting from ProofGeneral</title>
    21.7 +    <link rel="stylesheet" type="text/css" href="/basic.css"/>
    21.8 +  </head>
    21.9 +  <body>
   21.10 +    <h1>Pasting theory text from Proof General</h1>
   21.11 +    <ol>
   21.12 +      <li>Select the text using the keyboard (<code>C-SPC</code>, 
   21.13 +      <code>arrow keys</code>).</li>
   21.14 +      <li>Choose <code>X-Symbol</code>/<code>Other 
   21.15 +        Commands</code>/<code>Copy Encoded</code>.</li>
   21.16 +      <li>Paste into the web browser (<code>C-v</code>).</li>
   21.17 +    </ol>
   21.18 +
   21.19 +    <a href="/isabelle/find_theorems">Return to find_theorems</a>
   21.20 +  </body>
   21.21 +</html>
   21.22 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Tools/WWW_Find/xhtml.ML	Fri Nov 20 18:36:44 2009 +1100
    22.3 @@ -0,0 +1,438 @@
    22.4 +(*  Title:      xhtml.ML
    22.5 +    Author:     Timothy Bourke, NICTA
    22.6 +
    22.7 +Rudimentary XHTML construction.
    22.8 +*)
    22.9 +signature XHTML =
   22.10 +sig
   22.11 +  type attribute
   22.12 +  type common_atts = { id : string option,
   22.13 +                       class : string option };
   22.14 +  val noid : common_atts;
   22.15 +  val id : string -> common_atts;
   22.16 +  val class : string -> common_atts;
   22.17 +
   22.18 +  type tag
   22.19 +
   22.20 +  val doctype_xhtml1_0_strict: string;
   22.21 +
   22.22 +  val att: string -> string -> attribute
   22.23 +  val bool_att: string * bool -> attribute list
   22.24 +
   22.25 +  val tag: string -> attribute list -> tag list -> tag
   22.26 +  val tag': string -> common_atts -> tag list -> tag
   22.27 +  val text: string -> tag
   22.28 +  val raw_text: string -> tag
   22.29 +
   22.30 +  val add_attributes: attribute list -> tag -> tag
   22.31 +  val append: tag -> tag list -> tag
   22.32 +
   22.33 +  val show: tag -> string list
   22.34 +
   22.35 +  val write: (string -> unit) -> tag -> unit
   22.36 +  val write_open: (string -> unit) -> tag -> unit
   22.37 +  val write_close: (string -> unit) -> tag -> unit
   22.38 +
   22.39 +  val html: { lang : string } -> tag list -> tag
   22.40 +  val head: { title : string, stylesheet_href : string } -> tag list -> tag
   22.41 +  val body: common_atts -> tag list -> tag
   22.42 +  val divele: common_atts -> tag list -> tag
   22.43 +  val span: common_atts * string -> tag
   22.44 +  val span': common_atts -> tag list -> tag
   22.45 +
   22.46 +  val pre: common_atts -> string -> tag
   22.47 +
   22.48 +  val table: common_atts -> tag list -> tag
   22.49 +  val thead: common_atts -> tag list -> tag
   22.50 +  val tbody: common_atts -> tag list -> tag
   22.51 +  val tr: tag list -> tag
   22.52 +  val th: common_atts * string -> tag
   22.53 +  val th': common_atts -> tag list -> tag
   22.54 +  val td: common_atts * string -> tag
   22.55 +  val td': common_atts -> tag list -> tag
   22.56 +  val td'': common_atts * { colspan : int option, rowspan : int option }
   22.57 +           -> tag list -> tag
   22.58 +
   22.59 +  val p: common_atts * string -> tag
   22.60 +  val p': common_atts * tag list -> tag
   22.61 +  val h: common_atts * int * string -> tag
   22.62 +  val strong: string -> tag
   22.63 +  val em: string -> tag
   22.64 +  val a: { href : string, text : string } -> tag
   22.65 +
   22.66 +  val ul: common_atts * tag list -> tag
   22.67 +  val ol: common_atts * tag list -> tag
   22.68 +  val dl: common_atts * (string * tag) list -> tag
   22.69 +
   22.70 +  val alternate_class: { class0 : string, class1 : string }
   22.71 +                      -> tag list -> tag list
   22.72 +
   22.73 +  val form: common_atts * { method : string, action : string }
   22.74 +            -> tag list -> tag
   22.75 +
   22.76 +  datatype input_type =
   22.77 +      TextInput of { value: string option, maxlength: int option }
   22.78 +    | Password of int option
   22.79 +    | Checkbox of { checked : bool, value : string option }
   22.80 +    | Radio of { checked : bool, value : string option }
   22.81 +    | Submit
   22.82 +    | Reset
   22.83 +    | Hidden
   22.84 +    | Image of { src : string, alt : string }
   22.85 +    | File of { accept : string }
   22.86 +    | Button;
   22.87 +
   22.88 +  val input: common_atts * { name : string, itype : input_type } -> tag
   22.89 +  val select: common_atts * { name : string, value : string option }
   22.90 +              -> string list -> tag
   22.91 +  val label: common_atts * { for: string } * string -> tag
   22.92 +
   22.93 +  val reset_button: common_atts -> tag
   22.94 +  val submit_button: common_atts -> tag
   22.95 +
   22.96 +  datatype event =
   22.97 +    (* global *)
   22.98 +      OnClick
   22.99 +    | OnDblClick
  22.100 +    | OnMouseDown
  22.101 +    | OnMouseUp
  22.102 +    | OnMouseOver
  22.103 +    | OnMouseMove
  22.104 +    | OnMouseOut
  22.105 +    | OnKeyPress
  22.106 +    | OnKeyDown
  22.107 +    | OnKeyUp
  22.108 +      (* anchor/label/input/select/textarea/button/area *)
  22.109 +    | OnFocus
  22.110 +    | OnBlur
  22.111 +      (* form *)
  22.112 +    | OnSubmit
  22.113 +    | OnReset
  22.114 +      (* input/textarea *)
  22.115 +    | OnSelect
  22.116 +      (* input/select/textarea *)
  22.117 +    | OnChange
  22.118 +      (* body *)
  22.119 +    | OnLoad
  22.120 +    | OnUnload;
  22.121 +
  22.122 +  val script: common_atts * { script_type: string, src: string } -> tag
  22.123 +  val add_script: event * string -> tag -> tag
  22.124 +end;
  22.125 +
  22.126 +structure Xhtml : XHTML =
  22.127 +struct
  22.128 +
  22.129 +type attribute = string * string;
  22.130 +type common_atts = {
  22.131 +    id : string option,
  22.132 +    class : string option
  22.133 +  };
  22.134 +val noid = { id = NONE, class = NONE };
  22.135 +fun id s = { id = SOME s, class = NONE };
  22.136 +fun class s = { id = NONE, class = SOME s };
  22.137 +
  22.138 +fun from_common { id = NONE,   class = NONE } = []
  22.139 +  | from_common { id = SOME i, class = NONE } = [("id", i)]
  22.140 +  | from_common { id = NONE,   class = SOME c } = [("class", c)]
  22.141 +  | from_common { id = SOME i, class = SOME c } = [("id", i), ("class", c)];
  22.142 +
  22.143 +val update_atts =
  22.144 +  AList.join (op = : string * string -> bool) (fn _ => snd);
  22.145 +
  22.146 +datatype tag = Tag of (string * attribute list * tag list)
  22.147 +             | Text of string
  22.148 +             | RawText of string;
  22.149 +
  22.150 +fun is_text (Tag _) = false
  22.151 +  | is_text (Text _) = true
  22.152 +  | is_text (RawText _) = true;
  22.153 +
  22.154 +fun is_tag (Tag _) = true
  22.155 +  | is_tag (Text _) = false
  22.156 +  | is_tag (RawText _) = false;
  22.157 +
  22.158 +val att = pair;
  22.159 +
  22.160 +fun bool_att (nm, true) = [(nm, nm)]
  22.161 +  | bool_att (nm, false) = [];
  22.162 +
  22.163 +fun tag name atts inner = Tag (name, atts, inner);
  22.164 +fun tag' name common_atts inner = Tag (name, from_common common_atts, inner);
  22.165 +fun text t = Text t;
  22.166 +fun raw_text t = RawText t;
  22.167 +
  22.168 +fun add_attributes atts' (Tag (nm, atts, inner)) =
  22.169 +      Tag (nm, update_atts (atts, atts'), inner)
  22.170 +  | add_attributes _ t = t;
  22.171 +
  22.172 +fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
  22.173 +  | append _ _ = raise Fail "cannot append to a text element";
  22.174 +
  22.175 +fun show_att (n, v) = concat [" ", n, "=\"", XML.text v, "\""];
  22.176 +
  22.177 +fun show_text (Text t) = XML.text t
  22.178 +  | show_text (RawText t) = t
  22.179 +  | show_text _ = raise Fail "Bad call to show_text.";
  22.180 +
  22.181 +fun show (Text t) = [XML.text t]
  22.182 +  | show (RawText t) = [t]
  22.183 +  | show (Tag (nm, atts, inner)) =
  22.184 +  (["<", nm] @ map show_att atts
  22.185 +   @
  22.186 +   (if length inner = 0
  22.187 +    then ["/>"]
  22.188 +    else List.concat (
  22.189 +      [[">"]]
  22.190 +      @
  22.191 +      map show inner
  22.192 +      @
  22.193 +      [["</", nm, ">"]]
  22.194 +  )));
  22.195 +
  22.196 +fun write pr =
  22.197 +  let
  22.198 +    fun f (Text t) = (pr o XML.text) t
  22.199 +      | f (RawText t) = pr t
  22.200 +      | f (Tag (nm, atts, inner)) = (
  22.201 +          pr "<";
  22.202 +          pr nm;
  22.203 +          app (pr o show_att) atts;
  22.204 +          if length inner = 0
  22.205 +          then pr "/>"
  22.206 +          else (
  22.207 +            pr ">";
  22.208 +            app f inner;
  22.209 +            pr ("</" ^ nm ^ ">")
  22.210 +          ))
  22.211 +  in f end;
  22.212 +
  22.213 +(* Print all opening tags down into the tree until a branch of degree > 1 is
  22.214 +   found, in which case print everything before the last tag, which is then
  22.215 +   opened. *)
  22.216 +fun write_open pr =
  22.217 +  let
  22.218 +    fun f (Text t) = (pr o XML.text) t
  22.219 +      | f (RawText t) = pr t
  22.220 +      | f (Tag (nm, atts, [])) =
  22.221 +          (pr "<"; pr nm; app (pr o show_att) atts; pr ">")
  22.222 +      | f (Tag (nm, atts, xs)) =
  22.223 +           (pr "<"; pr nm; app (pr o show_att) atts; pr ">";
  22.224 +            (case take_suffix is_text xs of
  22.225 +               ([], _) => ()
  22.226 +             | (b, _) =>
  22.227 +                 let val (xs, x) = split_last b;
  22.228 +                 in app (write pr) xs; f x end));
  22.229 +  in f end;
  22.230 +
  22.231 +(* Print matching closing tags for write_open. *)
  22.232 +fun write_close pr =
  22.233 +  let
  22.234 +    fun close nm = pr ("</" ^ nm ^ ">");
  22.235 +    val pr_text = app (pr o show_text);
  22.236 +
  22.237 +    fun f (Text t) = ()
  22.238 +      | f (RawText t) = ()
  22.239 +      | f (Tag (nm, _, [])) = close nm
  22.240 +      | f (Tag (nm, _, xs)) =
  22.241 +           (case take_suffix is_text xs of
  22.242 +              ([], text) => pr_text text
  22.243 +            | (b, text) =>
  22.244 +                let val (xs, x) = split_last b;
  22.245 +                in f x; close nm; pr_text text end);
  22.246 +  in f end;
  22.247 +
  22.248 +fun html { lang } tags = Tag ("html",
  22.249 +                              [("xmlns", "http://www.w3.org/1999/xhtml"),
  22.250 +                               ("xml:lang", lang)],
  22.251 +                              tags);
  22.252 +
  22.253 +fun head { title, stylesheet_href } inner = let
  22.254 +    val link =
  22.255 +      Tag ("link",
  22.256 +        [("rel", "stylesheet"),
  22.257 +         ("type", "text/css"),
  22.258 +         ("href", stylesheet_href)], []);
  22.259 +    val title = Tag ("title", [], [Text title]);
  22.260 +    val charset = Tag ("meta",
  22.261 +        [("http-equiv", "Content-type"),
  22.262 +         ("content", "text/html; charset=UTF-8")], []);
  22.263 +  in Tag ("head", [], link::title::charset::inner) end;
  22.264 +
  22.265 +fun body common_atts tags = Tag ("body", from_common common_atts, tags);
  22.266 +
  22.267 +fun divele common_atts tags = Tag ("div", from_common common_atts, tags);
  22.268 +fun span (common_atts, t) = Tag ("span", from_common common_atts, [Text t]);
  22.269 +fun span' common_atts tags = Tag ("span", from_common common_atts, tags);
  22.270 +
  22.271 +fun pre common_atts rt = Tag ("pre", from_common common_atts, [RawText rt]);
  22.272 +
  22.273 +fun ostr_att (nm, NONE) = []
  22.274 +  | ostr_att (nm, SOME s) = [(nm, s)];
  22.275 +val oint_att = ostr_att o apsnd (Option.map Int.toString);
  22.276 +
  22.277 +val table = tag' "table";
  22.278 +val thead = tag' "thead";
  22.279 +val tbody = tag' "tbody";
  22.280 +val tr = tag "tr" [];
  22.281 +fun th (common_atts, t) = Tag ("th", from_common common_atts, [Text t]);
  22.282 +fun th' common_atts tags = Tag ("th", from_common common_atts, tags);
  22.283 +fun td (common_atts, t) = Tag ("td", from_common common_atts, [Text t]);
  22.284 +fun td' common_atts tags = Tag ("td", from_common common_atts, tags);
  22.285 +fun td'' (common_atts, { colspan, rowspan }) tags =
  22.286 +  Tag ("td",
  22.287 +    from_common common_atts
  22.288 +    @ oint_att ("colspan", colspan)
  22.289 +    @ oint_att ("rowspan", rowspan),
  22.290 +    tags);
  22.291 +
  22.292 +fun p (common_atts, t) = Tag ("p", from_common common_atts, [Text t]);
  22.293 +fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags);
  22.294 +
  22.295 +fun h (common_atts, i, text) =
  22.296 +  Tag ("h" ^ Int.toString i, from_common common_atts, [Text text]);
  22.297 +
  22.298 +fun strong t = Tag ("strong", [], [Text t]);
  22.299 +fun em t = Tag ("em", [], [Text t]);
  22.300 +fun a { href, text } = Tag ("a", [("href", href)], [Text text]);
  22.301 +
  22.302 +fun to_li tag = Tag ("li", [], [tag]);
  22.303 +fun ul (common_atts, lis) = Tag ("ul", from_common common_atts, map to_li lis);
  22.304 +fun ol (common_atts, lis) = Tag ("ol", from_common common_atts, map to_li lis);
  22.305 +
  22.306 +fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
  22.307 +                         Tag ("dd", [], [tag])];
  22.308 +fun dl (common_atts, dtdds) =
  22.309 +  Tag ("dl", from_common common_atts, (List.concat o map to_dtdd) dtdds);
  22.310 +            
  22.311 +fun alternate_class { class0, class1 } rows = let
  22.312 +    fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)
  22.313 +      | f ((false, xs), x) = (true, add_attributes [("class", class1)] x :: xs);
  22.314 +  in Library.foldl f ((true, []), rows) |> snd |> rev end;
  22.315 +
  22.316 +fun form (common_atts as { id, ... }, { method, action }) tags =
  22.317 +  Tag ("form",
  22.318 +    [("method", method),
  22.319 +     ("action", action)]
  22.320 +    @ from_common common_atts, tags);
  22.321 +
  22.322 +datatype input_type =
  22.323 +    TextInput of { value: string option, maxlength: int option }
  22.324 +  | Password of int option
  22.325 +  | Checkbox of { checked : bool, value : string option }
  22.326 +  | Radio of { checked : bool, value : string option }
  22.327 +  | Submit
  22.328 +  | Reset
  22.329 +  | Hidden
  22.330 +  | Image of { src : string, alt : string }
  22.331 +  | File of { accept : string }
  22.332 +  | Button;
  22.333 +
  22.334 +fun from_checked { checked = false, value = NONE }   = []
  22.335 +  | from_checked { checked = true,  value = NONE }   = [("checked", "checked")]
  22.336 +  | from_checked { checked = false, value = SOME v } = [("value", v)]
  22.337 +  | from_checked { checked = true,  value = SOME v } =
  22.338 +      [("checked", "checked"), ("value", v)];
  22.339 +
  22.340 +fun input_atts (TextInput { value, maxlength }) =
  22.341 +      ("type", "text")
  22.342 +       :: ostr_att ("value", value)
  22.343 +        @ oint_att ("maxlength", maxlength)
  22.344 +  | input_atts (Password NONE) = [("type", "password")]
  22.345 +  | input_atts (Password (SOME i)) =
  22.346 +      [("type", "password"), ("maxlength", Int.toString i)]
  22.347 +  | input_atts (Checkbox checked) =
  22.348 +      ("type", "checkbox") :: from_checked checked
  22.349 +  | input_atts (Radio checked) = ("type", "radio") :: from_checked checked
  22.350 +  | input_atts Submit = [("type", "submit")]
  22.351 +  | input_atts Reset = [("type", "reset")]
  22.352 +  | input_atts Hidden = [("type", "hidden")]
  22.353 +  | input_atts (Image { src, alt }) =
  22.354 +      [("type", "image"), ("src", src), ("alt", alt)]
  22.355 +  | input_atts (File { accept }) = [("type", "file"), ("accept", accept)]
  22.356 +  | input_atts Button = [("type", "button")];
  22.357 +
  22.358 +fun input (common_atts, { name, itype }) =
  22.359 +  Tag ("input",
  22.360 +       input_atts itype @ [("name", name)] @ from_common common_atts,
  22.361 +       []);
  22.362 +
  22.363 +fun reset_button common_atts =
  22.364 +  Tag ("input", input_atts Reset @ from_common common_atts, []);
  22.365 +
  22.366 +fun submit_button common_atts =
  22.367 +  Tag ("input", input_atts Submit @ from_common common_atts, []);
  22.368 +
  22.369 +
  22.370 +fun select (common_atts, { name, value }) options =
  22.371 +  let
  22.372 +    fun is_selected t =
  22.373 +      (case value of
  22.374 +         NONE => []
  22.375 +       | SOME s => if t = s then bool_att ("selected", true) else []);
  22.376 +    fun to_option t = Tag ("option", is_selected t, [Text t]);
  22.377 +  in
  22.378 +    Tag ("select",
  22.379 +      ("name", name) :: from_common common_atts,
  22.380 +      map to_option options)
  22.381 +  end;
  22.382 +
  22.383 +fun label (common_atts, { for }, text) =
  22.384 +  Tag ("label", ("for", for) :: from_common common_atts, [Text text]);
  22.385 +
  22.386 +datatype event =
  22.387 +    OnClick
  22.388 +  | OnDblClick
  22.389 +  | OnMouseDown
  22.390 +  | OnMouseUp
  22.391 +  | OnMouseOver
  22.392 +  | OnMouseMove
  22.393 +  | OnMouseOut
  22.394 +  | OnKeyPress
  22.395 +  | OnKeyDown
  22.396 +  | OnKeyUp
  22.397 +  | OnFocus
  22.398 +  | OnBlur
  22.399 +  | OnSubmit
  22.400 +  | OnReset
  22.401 +  | OnSelect
  22.402 +  | OnChange
  22.403 +  | OnLoad
  22.404 +  | OnUnload;
  22.405 +
  22.406 +fun event_to_str OnClick = "onclick"
  22.407 +  | event_to_str OnDblClick = "ondblclick"
  22.408 +  | event_to_str OnMouseDown = "onmousedown"
  22.409 +  | event_to_str OnMouseUp = "onmouseup"
  22.410 +  | event_to_str OnMouseOver = "onmouseover"
  22.411 +  | event_to_str OnMouseMove = "onmousemove"
  22.412 +  | event_to_str OnMouseOut = "onmouseout"
  22.413 +  | event_to_str OnKeyPress = "onkeypress"
  22.414 +  | event_to_str OnKeyDown = "onkeydown"
  22.415 +  | event_to_str OnKeyUp = "onkeyup"
  22.416 +  | event_to_str OnFocus = "onfocus"
  22.417 +  | event_to_str OnBlur = "onblur"
  22.418 +  | event_to_str OnSubmit = "onsubmit"
  22.419 +  | event_to_str OnReset = "onreset"
  22.420 +  | event_to_str OnSelect = "onselect"
  22.421 +  | event_to_str OnChange = "onchange"
  22.422 +  | event_to_str OnLoad = "onload"
  22.423 +  | event_to_str OnUnload = "onunload";
  22.424 +
  22.425 +fun script (common_atts, {script_type, src}) =
  22.426 +  Tag ("script",
  22.427 +    ("type", script_type)
  22.428 +    :: ("src", src)
  22.429 +    :: from_common common_atts, [text ""]);
  22.430 +
  22.431 +fun add_script (evty, script) (Tag (name, atts, inner))
  22.432 +      = Tag (name, AList.update (op =) (event_to_str evty, script) atts, inner)
  22.433 +  | add_script _ t = t;
  22.434 +
  22.435 +
  22.436 +val doctype_xhtml1_0_strict =
  22.437 +  "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
  22.438 +  \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
  22.439 +
  22.440 +end;
  22.441 +