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 +