--- a/etc/components Fri Nov 20 10:40:30 2009 +0100
+++ b/etc/components Fri Nov 20 18:36:44 2009 +1100
@@ -12,6 +12,7 @@
src/Sequents
#misc components
src/Tools/Code
+src/Tools/WWW_Find
src/HOL/Tools/ATP_Manager
src/HOL/Mirabelle
src/HOL/Library/Sum_Of_Squares
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/IsaMakefile Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,21 @@
+#
+# IsaMakefile for WWW_Find
+#
+# Provides static compile check for ML files only.
+
+
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+LOGFILE = $(LOG)/Pure-WWW_Find.gz
+
+all: test
+test: $(LOGFILE)
+
+$(LOGFILE): echo.ML find_theorems.ML html_unicode.ML \
+ http_status.ML http_util.ML mime.ML scgi_req.ML scgi_server.ML \
+ socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
+ cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
+
+clean:
+ rm -f $(LOGFILE)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/ROOT.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,14 @@
+if String.isPrefix "polyml" ml_system
+then
+ (use "unicode_symbols.ML";
+ use "html_unicode.ML";
+ use "mime.ML";
+ use "http_status.ML";
+ use "http_util.ML";
+ use "xhtml.ML";
+ use "socket_util.ML";
+ use "scgi_req.ML";
+ use "scgi_server.ML";
+ use "echo.ML";
+ use "find_theorems.ML")
+else ()
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/doc/README Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,28 @@
+Requirements
+------------
+ lighttpd
+ polyml (other ML systems untested)
+
+Quick setup
+-----------
+* install lighttpd if necessary
+ (and optionally disable automatic startup on default www port)
+
+Quick instructions
+------------------
+* start the server with:
+ isabelle wwwfind start
+ (add -l for logging from ML)
+
+* connect (by default) on port 8000:
+ http://localhost:8000/isabelle/find_theorems
+
+* test with the echo server:
+ http://localhost:8000/isabelle/echo
+
+* check the status with:
+ isabelle wwwfind status
+
+* stop the server with:
+ isabelle wwwfind stop
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/doc/design.tex Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,330 @@
+% $Id$
+%
+% vim:nojs: tw=76 sw=4 sts=4 fo=awn fdm=marker
+%
+% 20090406 T. Bourke
+% Original document.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\documentclass[a4paper,draft]{article} % XXX
+%\documentclass[a4paper,final]{article}
+% Preamble
+\usepackage[T1]{fontenc}
+\usepackage{textcomp}
+\usepackage{ifdraft}
+
+\bibliographystyle{abbrv} % alpha
+
+\newcommand{\refsec}[1]{Section~\ref{sec:#1}}
+\newcommand{\reffig}[1]{Figure~\ref{fig:#1}}
+\newcommand{\reftab}[1]{Table~\ref{tab:#1}}
+
+%
+\usepackage{acronym}
+\usepackage{pst-all}
+\usepackage{url}
+
+\title{Isabelle find\_theorems on the web}
+\author{T. Bourke\thanks{NICTA}}
+
+\special{!/pdfmark where
+ {pop} {userdict /pdfmark /cleartomark load put} ifelse
+ [ /Author (T. Bourke, NICTA)
+ /Title (IsabelleWWW: find_theorems
+ ($Date: 2008-10-03 16:09:02 +1000 (Fri, 03 Oct 2008) $))
+ /Subject (Web interface to find_theorems)
+ /Keywords (isabelle, sml, http, www)
+ /DOCINFO pdfmark}
+
+\begin{document}
+% Title page and abstract
+\maketitle
+
+\begin{abstract}
+The Isabelle find\_theorems command processes queries against a theory
+database and returns a list of matching theorems.
+It is usually given from the Proof General or command-line interface.
+This document describes a web server implementation.
+Two design alternatives are presented and an overview of an implementation
+of one is described.
+\end{abstract}
+
+\section{Introduction}\label{sec:intro}
+
+This document describes the design and implementation of a web interface for
+the Isabelle find\_theorems command.
+The design requirements and their consequences are detailed in \refsec{req}.
+Two architectures were considered: \begin{enumerate}
+
+\item \emph{one process}: integrate a web server into Isabelle.
+
+\item \emph{two processes}: run Isabelle as a web server module.
+
+\end{enumerate}
+A brief evaluation of the one process architecture is presented in
+\refsec{oneproc}.
+An implementation of the two process is presented in \refsec{twoproc}.
+
+\section{Design requirements}\label{sec:req}
+
+The main requirements are:\begin{enumerate}
+\item The system will allow users to search for theorems from a web browser.
+\item It will allow queries across disparate Isabelle theories.
+\item It will, at a minimum, handle theories from the L4.verified project.
+\item It will run on a secure network.
+\item There will be at most ten simultaneous users.
+\end{enumerate}
+
+\noindent
+Several \emph{a priori} choices are fixed:\begin{enumerate}
+\item The search will run against an Isabelle heap.
+\item A single heap will be built from the theories to be searched.
+\item The system must be persistent, for two reasons: \begin{enumerate}
+ \item Isabelle is slow to start against large heaps.
+ \item Later enhancements may require tracking states at the server.
+\end{enumerate}
+\end{enumerate}
+
+\section{Evaluation: Isabelle web server}\label{sec:oneproc}
+
+The advantage of integrating a web server into Isabelle is that the
+find\_theorems service could be provided by a single process, which, in
+principle, would simplify administration.
+Implementing even a simple \ac{HTTP} service from scratch is an unacceptable
+cost and fraught with potential problems and limitations.
+It is preferable to adapt an existing system.
+
+As Isabelle is written in \ac{SML}, only \ac{HTTP} services also written in
+\ac{SML} can realistically be considered.
+In principle Isabelle compiles on both Poly/ML and \ac{SML/NJ}, but in
+practice the former is faster, more widely used, and better supported.
+In particular, the L4.verified project does not build effectively on
+\ac{SML/NJ}.
+This further limits the potential to adapt an existing system.
+
+There are three \ac{SML} web server projects:\\
+\centerline{\begin{tabular}{ll}
+SMLServer &
+ \url{http://www.smlserver.org}\\
+FoxNet web server &
+ \url{http://www.cs.cmu.edu/~fox/}\\
+Swerve web server &
+ \url{http://mlton.org/Swerve}
+\end{tabular}}
+
+Unfortunately, none of these projects is suitable.
+
+The SMLServer is an Apache web server plugin.
+It runs \ac{SML} programs that generate dynamic web pages.
+SMLServer is based on the MLKit compiler.
+It is unlikely that Isabelle and the l4.verified heaps could be compiled in
+MLKit, at least not without significant effort.
+
+The FoxNet web server was developed as part of the Fox project at \ac{CMU}.
+The source is not readily available.
+
+The Swerve web server is part of an unpublished book on systems programming
+in \ac{SML}.
+The source code is available and it is readily patched to run under the
+latest version of SML/NJ (110.67).
+Adapting it to Poly/ML would require non-trivial effort because it is based
+on \ac{CML}, whose implementation on SML/NJ makes use of continuations
+(SMLofNJ.cont).
+
+\section{Implementation: Isabelle web module}\label{sec:twoproc}
+
+The description of the two process solution is divided into two subsections.
+The first contains an overview of the architecture and web server specifics.
+The second contains a summary of an \ac{SML} implementation of the web
+module in Isabelle.
+
+\subsection{Architecture and web server}\label{sec:oneproc:arch}
+
+\newcommand{\component}[1]{%
+ \rput(0,0){\psframe(-.8,-.6)(.8,.6)}%
+ \rput(0,0){\parbox{4.3em}{\centering{#1}}}}
+
+\begin{figure}
+\centering%
+\begin{pspicture}(-4.8,0)(3.3,4)%\psgrid
+ \newpsstyle{conn}{arrows=->}%
+ %
+ \rput(-2.2,3.3){\component{web server}}%
+ \rput( 2.2,3.3){\component{web module}}%
+ \rput(-2.2,0.7){\component{web client}}%
+ \rput(-4.2,3.4){%
+ \psellipse(0,-.2)(.4,.2)%
+ \psframe[linestyle=none,fillstyle=solid,fillcolor=white]%
+ (-.4,-.2)(.4,.1)%
+ \psellipse(0,.1)(.4,.2)%
+ \psline(-.38,-.2)(-.38,.1)\psline(.38,-.2)(.38,.1)%
+ }%
+ \psline[style=conn,arrows=<->](-3.0,3.3)(-3.8,3.3)%
+ %
+ \rput[rB](3.3,2.15){server}%
+ \psline[linestyle=dashed](-4.8,2)(3.3,2)%
+ \rput[rt](3.3,1.90){network}%
+ %
+ \rput[B](0.0,3.55){\psframebox*{module protocol}}%
+ \psline[style=conn](-1.4,3.4)(1.4,3.4)%
+ \psline[style=conn](1.4,3.2)(-1.4,3.2)%
+ %
+ \rput[B]{90}(-2.4,2.0){\psframebox*{\ac{HTTP}}}%
+ \psline[style=conn](-2.1,2.7)(-2.1,1.3)%
+ \psline[style=conn](-2.3,1.3)(-2.3,2.7)%
+\end{pspicture}
+\caption{Overview of web module architecture\label{fig:modulearch}}
+\end{figure}
+
+An overview of a simple web server architecture is presented in
+\reffig{modulearch}.
+A \emph{web client} requests a \ac{URL} from a \emph{web server} over
+\ac{HTTP}.
+The web server processes the request by fetching static elements from its
+local file system and communicating with \emph{web modules} to dynamically
+generate other elements.
+The elements are sent back across the network to the web client.
+
+The web server communicates with web modules over a \emph{module protocol},
+which dictates a means of passing requests and receiving responses.
+There are several common module protocols.
+
+In the \ac{CGI}, the web server executes processes to service dynamic
+\acp{URL}.
+Request details are placed in environment variables and sent on the standard
+input channels of processes, responses are read from the standard output
+channels of processes and transmitted back to web clients.
+
+The chief disadvantage of \ac{CGI} is that it creates a new process for
+every request.
+Fast \ac{CGI} web modules, on the other hand, run persistently in a loop.
+They receive and respond to web server requests over a duplex socket.
+The Fast \ac{CGI} protocol is quite complicated.
+There are, however, alternatives like \ac{SCGI} that are easier for web
+modules to support.
+This is important when programming in \ac{SML} because both the number of
+developers and available libraries are small.
+
+An \ac{SCGI} web module listens on a socket for requests from a web server.
+Requests are sent as stream of bytes.
+The first part of the request is a null-delimited sequence of name and value
+pairs.
+The second part is unparsed text sent from the web client.
+The web module responds by sending text, usually \ac{HTTP} headers followed
+by \ac{HTML} data, back over the socket.
+The whole protocol can be described in two
+pages.\footnote{\url{http://python.ca/scgi/protocol.txt}}
+
+Both the Apache and Lighttpd web servers support the \ac{SCGI} protocol.
+Lighttpd was chosen because it seemed to be small, fast, and easy to
+configure.
+Two settings are required to connect lighttpd to an \ac{SCGI} web module:
+\begin{verbatim}
+server.modules = ( "mod_scgi" )
+scgi.server = ("/isabelle" => ((
+ "host" => "127.0.0.1",
+ "port" => 64000,
+ "check-local" => "disable")))
+\end{verbatim}
+In this example, the \texttt{scgi.server} entry directs the web server to
+pass all \acp{URL} beginning with \texttt{/isabelle} to the web module
+listening on port \texttt{64000}.
+
+\subsection{Implementation in \acs{SML}}\label{sec:oneproc:impl}
+
+\begin{table}
+\begin{tabular}{lp{.70\textwidth}}
+\textbf{Module} & \textbf{Description}\\\hline
+Mime & Rudimentary support for mime types.\\
+HttpStatus & \ac{HTTP} header status codes.\\
+HttpUtil & Produce \ac{HTTP} headers and parse query strings.\\
+Xhtml & Rudimentary support for generating \ac{HTML}.\\
+SocketUtil & Routines from The Standard ML Basis Library
+ book.\footnote{Chapter 10, Gansner and Reppy,
+ Cambridge University Press.}\\
+\textbf{ScgiReq} & Parse \ac{SCGI} requests.\\
+\textbf{ScgiServer} & \ac{SCGI} server event loop and dispatch.\\
+\textbf{FindTheorems}& \ac{HTML} interface to find\_theorems.
+\end{tabular}
+\caption{Web module implementation\label{tab:moduleimpl}}
+\end{table}
+
+The find\_theorems web module is implemented in \ac{SML}.
+It uses elements of the Pure library in Isabelle.
+The program comprises the nine modules shown in \reftab{moduleimpl}.
+The three most important ones are shown in bold: ScgiReq, ScgiServer, and
+FindTheorems.
+
+ScgiReq implements the client-side of the \ac{SCGI} protocol.
+It maps a binary input stream into a request data type.
+
+ScgiServer is a generic, multi-threaded \ac{SCGI} request dispatcher.
+It accepts \ac{SCGI} requests on a designated socket, selects an appropriate
+handler from an internal list, and calls the handler in a new thread.
+
+FindTheorems registers a handler with ScgiServer.
+It parses \ac{SCGI}/\ac{HTTP} requests, calls the Isabelle find\_theorems
+function, and returns the results as \ac{HTML}.
+The \ac{HTML} generation of individual theorems is handled by the \ac{HTML}
+print mode of Isabelle, but the form fields and page structure were manually
+implemented.
+
+The module is built by using a \texttt{ROOT.ML} file inside a heap that
+contains the theories to be searched.
+The server is started by calling \texttt{ScgiServer.server}.
+Scripts have been created to automate this process.
+
+\subsection{Handling symbols}\label{sec:unicode}
+
+Isabelle theorems are usually written in mathematical notation.
+Internally, however, Isabelle only manipulates \acs{ASCII} strings.
+Symbols are encoded by strings that begin with a backslash and contain a
+symbol name between angle braces, for example, the symbol~$\longrightarrow$
+becomes~\verb+\<longrightarrow>+.
+The existing Thy/Html module in the Isabelle Pure theory converts many of
+these symbols to \ac{HTML} entities.
+Custom routines are required to convert the missing symbols to \ac{HTML}
+\emph{numeric character references}, which are the Unicode codepoints of
+symbols printed in decimal between \verb+&#+ and \verb+;+.
+Further, other routines were required for converting \acs{UTF-8} encoded
+strings sent from web browsers into Isabelle's symbol encoding.
+
+Isabelle is distributed with a text file that maps Isabelle symbols to
+Unicode codepoints.
+A module was written to parse this file into symbol tables that map back and
+forth between Isabelle symbols and Unicode codepoints, and also between
+Isabelle \acs{ASCII} abbreviations (like \verb+-->+ for $\longrightarrow$)
+and Unicode codepoints.
+
+The conversion from Isabelle symbols to \ac{HTML} numeric character
+references is handled by a new printing mode, which is based in large part
+on the existing \ac{HTML} printing mode.
+The new mode is used in combination with the existing \texttt{xsymbol} mode,
+to ensure that Isabelle symbols are used instead of \acs{ASCII}
+abbreviations.
+
+The conversion from \acs{UTF-8} is handled by a custom routine.
+Additionally, there is a JavaScript routine that converts from Isabelle
+symbol encodings to \acs{UTF-8}, so that users can conveniently view
+manually-entered or pasted mathematical characters in the web browser
+interface.
+
+\section{Abbreviations}\label{sec:abbr}
+
+\begin{acronym}[SML/NJ] % longest acronym here
+ \acro{ASCII}{American Standard Code for Information Interchange}
+ \acro{CGI}{Common Gateway Interface}
+ \acro{CML}{Concurrent ML}
+ \acro{CMU}{Carnegie Mellon University}
+ \acro{HTML}{Hyper Text Markup Language}
+ \acro{HTTP}{Hyper Text Transfer Protocol}
+ \acro{ML}{Meta Language}
+ \acro{SCGI}{Simple CGI}
+ \acro{SML}{Standard ML}
+ \acro{SML/NJ}{Standard ML of New Jersey}
+ \acro{URL}{Universal Resource Locator}
+ \acro{UTF-8}{8-bit Unicode Transformation Format}
+ \acro{WWW}{World Wide Web}
+\end{acronym}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/echo.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,16 @@
+(* Title: echo.ML
+ Author: Timothy Bourke, NICTA
+
+ Install simple echo server.
+*)
+
+local
+fun echo (req, content, send) =
+ (send (ScgiReq.show req);
+ send "--payload-----\n";
+ send (Byte.bytesToString content);
+ send "\n--------------\n")
+in
+val () = ScgiServer.register ("echo", SOME Mime.plain, echo);
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/etc/settings Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,7 @@
+# the path to lighttpd
+LIGHTTPD="/usr/sbin/lighttpd"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+
+WWWFINDDIR="$COMPONENT"
+WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/find_theorems.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,244 @@
+(* Title: find_theorems.ML
+ Author: Timothy Bourke, NICTA
+
+ Simple find_theorems server
+*)
+
+local
+val default_limit = 20;
+val thy_names = sort string_ord (ThyInfo.get_names ());
+
+val find_theorems_url = "find_theorems";
+
+fun is_sorry thm =
+ Thm.proof_of thm
+ |> Proofterm.approximate_proof_body
+ |> Proofterm.all_oracles_of
+ |> exists (fn (x, _) => x = "Pure.skip_proof");
+
+local open Xhtml in
+fun find_theorems_form thy_name (query, limit, withdups) =
+ let
+ val query_input =
+ input (id "query", {
+ name = "query",
+ itype = TextInput { value = query, maxlength = NONE }});
+
+ val max_results = divele noid
+ [
+ label (noid, { for = "limit" }, "Max. results:"),
+ input (id "limit",
+ { name = "limit",
+ itype = TextInput { value = SOME (Int.toString limit),
+ maxlength = NONE }})
+ ];
+
+ val theories = divele noid
+ [
+ label (noid, { for = "theory" }, "Search in:"),
+ select (id "theory", { name = "theory", value = SOME thy_name })
+ thy_names
+ ];
+
+ val with_dups = divele noid
+ [
+ label (noid, { for = "withdups" }, "Allow duplicates:"),
+ input (id "withdups",
+ { name = "withdups",
+ itype = Checkbox { checked = withdups, value = SOME "true" }})
+ ];
+
+ val help = divele (class "help")
+ [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
+ in
+ form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
+ [tag "fieldset" []
+ [tag "legend" [] [text "find_theorems"],
+ (add_script (OnKeyPress, "encodequery(this)")
+ o add_script (OnChange, "encodequery(this)")
+ o add_script (OnMouseUp, "encodequery(this)")) query_input,
+ divele (class "settings") [ max_results, theories, with_dups, help ],
+ divele (class "mainbuttons")
+ [ reset_button (id "reset"), submit_button (id "submit") ]
+ ]
+ ]
+ end;
+
+fun html_header thy_name args =
+ html { lang = "en" } [
+ head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
+ [script (noid, { script_type="text/javascript",
+ src="/find_theorems.js" })],
+ add_script (OnLoad, "encodequery(document.getElementById('query'))")
+ (body noid [
+ h (noid, 1, "Theory " ^ thy_name),
+ find_theorems_form thy_name args,
+ divele noid []
+ ])
+ ];
+
+fun html_error msg = p ((class "error"), msg);
+
+val find_theorems_table =
+ table (class "findtheorems")
+ [
+ thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
+ tbody noid []
+ ];
+
+fun show_criterion (b, c) =
+ let
+ fun prfx s = let
+ val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
+ in span (class c, v) end;
+
+ fun prfxwith s = let
+ val (c, v) =
+ if b
+ then ("criterion", "with " ^ s)
+ else ("ncriterion", "without " ^ s);
+ in span (class c, v) end;
+ in
+ (case c of
+ Find_Theorems.Name name => prfx ("name: " ^ quote name)
+ | Find_Theorems.Intro => prfx "intro"
+ | Find_Theorems.IntroIff => prfx "introiff"
+ | Find_Theorems.Elim => prfx "elim"
+ | Find_Theorems.Dest => prfx "dest"
+ | Find_Theorems.Solves => prfx "solves"
+ | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
+ | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
+ end;
+
+fun find_theorems_summary (othmslen, thmslen, query, args) =
+ let
+ val args =
+ (case othmslen of
+ NONE => args
+ | SOME l => Symtab.update ("limit", Int.toString l) args)
+ val qargs = HttpUtil.make_query_string args;
+
+ val num_found_text =
+ (case othmslen of
+ NONE => text (Int.toString thmslen)
+ | SOME l =>
+ a { href = find_theorems_url ^
+ (if qargs = "" then "" else "?" ^ qargs),
+ text = Int.toString l })
+ val found = [text "found ", num_found_text, text " theorems"] : tag list;
+ val displayed =
+ if is_some othmslen
+ then " (" ^ Int.toString thmslen ^ " displayed)"
+ else "";
+ fun show_search c = tr [ td' noid [show_criterion c] ];
+ in
+ table (class "findtheoremsquery")
+ (* [ tr [ th (noid, "searched for:") ] ]
+ @ map show_search query @ *)
+ [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
+ end
+
+fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
+
+fun html_thm ctxt (n, (thmref, thm)) =
+ let
+ val string_of_thm =
+ Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
+ setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
+ in
+ tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
+ [
+ tag' "td" (class "name")
+ [span' (sorry_class thm)
+ [raw_text (Facts.string_of_ref thmref)]
+ ],
+ tag' "td" (class "thm") [pre noid (string_of_thm thm)]
+ ]
+ end;
+
+end;
+
+structure P = OuterParse
+ and K = OuterKeyword
+ and FT = Find_Theorems;
+
+val criterion =
+ P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
+ P.reserved "intro" >> K Find_Theorems.Intro ||
+ P.reserved "elim" >> K Find_Theorems.Elim ||
+ P.reserved "dest" >> K Find_Theorems.Dest ||
+ P.reserved "solves" >> K Find_Theorems.Solves ||
+ P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
+ P.term >> Find_Theorems.Pattern;
+
+val parse_query =
+ Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+
+fun app_index f xs = fold_index (fn x => K (f x)) xs ();
+
+fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
+ content, send) =
+ let
+ val arg_data =
+ (case request_method of
+ ScgiReq.Get => query_string
+ | ScgiReq.Post =>
+ content
+ |> Byte.bytesToString
+ |> HttpUtil.parse_query_string
+ | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
+
+ val args = Symtab.lookup arg_data;
+
+ val query = the_default "" (args "query");
+ fun get_query () =
+ query
+ |> (fn s => s ^ ";")
+ |> OuterSyntax.scan Position.start
+ |> filter OuterLex.is_proper
+ |> Scan.error parse_query
+ |> fst;
+
+ val limit =
+ args "limit"
+ |> Option.mapPartial Int.fromString
+ |> the_default default_limit;
+ val thy_name =
+ args "theory"
+ |> the_default "Main";
+ val with_dups = is_some (args "with_dups");
+
+ fun do_find () =
+ let
+ val ctxt = ProofContext.init (theory thy_name);
+ val query = get_query ();
+ val (othmslen, thms) = apsnd rev
+ (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
+ val thmslen = length thms;
+ fun thm_row args = Xhtml.write send (html_thm ctxt args);
+ in
+ Xhtml.write send
+ (find_theorems_summary (othmslen, thmslen, query, arg_data));
+ if null thms then ()
+ else (Xhtml.write_open send find_theorems_table;
+ HTML_Unicode.print_mode (app_index thm_row) thms;
+ Xhtml.write_close send find_theorems_table)
+ end;
+
+ val header = (html_header thy_name (args "query", limit, with_dups));
+ in
+ send Xhtml.doctype_xhtml1_0_strict;
+ Xhtml.write_open send header;
+ if query = "" then ()
+ else
+ do_find ()
+ handle
+ ERROR msg => Xhtml.write send (html_error msg)
+ | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
+ Xhtml.write_close send header
+ end;
+in
+val () = show_question_marks := false;
+val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/html_unicode.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,85 @@
+(* Title: html_unicode.ML
+ Author: Timothy Bourke, NICTA
+ Based on Pure/Thy/html.ML
+ by Markus Wenzel and Stefan Berghofer, TU Muenchen
+
+HTML presentation elements that use unicode code points.
+*)
+
+signature HTML_UNICODE =
+sig
+ val print_mode: ('a -> 'b) -> 'a -> 'b
+end;
+
+structure HTML_Unicode: HTML_UNICODE =
+struct
+
+(** HTML print modes **)
+
+(* mode *)
+
+val htmlunicodeN = "HTMLUnicode";
+fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
+
+(* symbol output *)
+
+local
+ val sym_width_lookup = Symtab.make
+ [("\<spacespace>", 2),
+ ("\<Longleftarrow>", 2),
+ ("\<longleftarrow>", 2),
+ ("\<Longrightarrow>", 2),
+ ("\<longrightarrow>", 2),
+ ("\<longleftrightarrow>", 2),
+ ("\<^bsub>", 0),
+ ("\<^esub>", 0),
+ ("\<^bsup>", 0),
+ ("\<^esup>", 0)];
+
+ fun sym_width s =
+ (case Symtab.lookup sym_width_lookup s of
+ NONE => 1
+ | SOME w => w);
+
+ fun output_sym s =
+ if Symbol.is_raw s then (1, Symbol.decode_raw s)
+ else
+ (case UnicodeSymbols.symbol_to_unicode s of
+ SOME x => (sym_width s, "&#" ^ Int.toString x ^ ";") (* numeric entities *)
+ (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x]) (* utf-8 *) *)
+ | NONE => (size s, XML.text s));
+
+ fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
+ fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
+ fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
+
+ fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
+ | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
+ | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
+ | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
+ | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
+ | output_syms (s :: ss) = output_sym s :: output_syms ss
+ | output_syms [] = [];
+
+ fun output_width str =
+ if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
+ then Output.default_output str
+ else
+ let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
+ (output_syms (Symbol.explode str)) 0
+ in (implode syms, width) end;
+in
+
+val output = #1 o output_width;
+
+val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw;
+
+end;
+
+(* common markup *)
+
+fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
+
+val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/http_status.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,157 @@
+(* Title: http_status.ML
+ Author: Timothy Bourke, NICTA
+
+HTTP status codes and reasons.
+*)
+signature HTTP_STATUS =
+sig
+ type t
+
+ val to_status_code : t -> int
+ val to_reason : t -> string
+ val from_status_code : int -> t option
+
+ val continue : t
+ val switching_protocols : t
+ val ok : t
+ val created : t
+ val accepted : t
+ val non_authoritative_information : t
+ val no_content : t
+ val reset_content : t
+ val partial_content : t
+ val multiple_choices : t
+ val moved_permanently : t
+ val found : t
+ val see_other : t
+ val not_modified : t
+ val use_proxy : t
+ val temporary_redirect : t
+ val bad_request : t
+ val unauthorized : t
+ val payment_required : t
+ val forbidden : t
+ val not_found : t
+ val method_not_allowed : t
+ val not_acceptable : t
+ val proxy_authentication_required : t
+ val request_timeout : t
+ val conflict : t
+ val gone : t
+ val length_required : t
+ val precondition_failed : t
+ val request_entity_too_large : t
+ val request_uri_too_long : t
+ val unsupported_media_type : t
+ val requested_range_not_satisfiable : t
+ val expectation_failed : t
+ val internal_server_error : t
+ val not_implemented : t
+ val bad_gateway : t
+ val service_unavailable : t
+ val gateway_timeout : t
+ val http_version_not_supported : t
+
+end;
+
+structure HttpStatus : HTTP_STATUS =
+struct
+
+type t = int
+
+local
+val int_status_map = Inttab.make
+ [(100, "Continue"),
+ (101, "Switching Protocols"),
+ (200, "OK"),
+ (201, "Created"),
+ (202, "Accepted"),
+ (203, "Non-Authoritative Information"),
+ (204, "No Content"),
+ (205, "Reset Content"),
+ (206, "Partial Content"),
+ (300, "Multiple Choices"),
+ (301, "Moved Permanently"),
+ (302, "Found"),
+ (303, "See Other"),
+ (304, "Not Modified"),
+ (305, "Use Proxy"),
+ (307, "Temporary Redirect"),
+ (400, "Bad Request"),
+ (401, "Unauthorized"),
+ (402, "Payment Required"),
+ (403, "Forbidden"),
+ (404, "Not Found"),
+ (405, "Method Not Allowed"),
+ (406, "Not Acceptable"),
+ (407, "Proxy Authentication Required"),
+ (408, "Request Timeout"),
+ (409, "Conflict"),
+ (410, "Gone"),
+ (411, "Length Required"),
+ (412, "Precondition Failed"),
+ (413, "Request Entity Too Large"),
+ (414, "Request URI Too Long"),
+ (415, "Unsupported Media Type"),
+ (416, "Requested Range Not Satisfiable"),
+ (417, "Expectation Failed"),
+ (500, "Internal Server Error"),
+ (501, "Not Implemented"),
+ (502, "Bad Gateway"),
+ (503, "Service Unavailable"),
+ (504, "Gateway Timeout"),
+ (505, "HTTP Version Not Supported")];
+in
+fun from_status_code i =
+ if is_some (Inttab.lookup int_status_map i)
+ then SOME i
+ else NONE;
+
+val to_reason = the o Inttab.lookup int_status_map;
+end;
+
+val to_status_code = I;
+
+val continue = 100;
+val switching_protocols = 101;
+val ok = 200;
+val created = 201;
+val accepted = 202;
+val non_authoritative_information = 203;
+val no_content = 204;
+val reset_content = 205;
+val partial_content = 206;
+val multiple_choices = 300;
+val moved_permanently = 301;
+val found = 302;
+val see_other = 303;
+val not_modified = 304;
+val use_proxy = 305;
+val temporary_redirect = 307;
+val bad_request = 400;
+val unauthorized = 401;
+val payment_required = 402;
+val forbidden = 403;
+val not_found = 404;
+val method_not_allowed = 405;
+val not_acceptable = 406;
+val proxy_authentication_required = 407;
+val request_timeout = 408;
+val conflict = 409;
+val gone = 410;
+val length_required = 411;
+val precondition_failed = 412;
+val request_entity_too_large = 413;
+val request_uri_too_long = 414;
+val unsupported_media_type = 415;
+val requested_range_not_satisfiable = 416;
+val expectation_failed = 417;
+val internal_server_error = 500;
+val not_implemented = 501;
+val bad_gateway = 502;
+val service_unavailable = 503;
+val gateway_timeout = 504;
+val http_version_not_supported = 505;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/http_util.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,94 @@
+(* Title: http_util.ML
+ Author: Timothy Bourke, NICTA
+
+Rudimentary utility functions for HTTP.
+*)
+signature HTTP_UTIL =
+sig
+ val crlf : string
+ val reply_header : HttpStatus.t * Mime.t option * (string * string) list -> string
+ val parse_query_string : string -> string Symtab.table
+ val make_query_string : string Symtab.table -> string
+end;
+
+structure HttpUtil : HTTP_UTIL =
+struct
+
+val crlf = "\r\n";
+
+fun make_header_field (name, value) = concat [name, ": ", value, crlf];
+
+fun reply_header (status, content_type, extra_fields) =
+ let
+ val code = (Int.toString o HttpStatus.to_status_code) status;
+ val reason = HttpStatus.to_reason status;
+ val show_content_type = pair "Content-Type" o Mime.show_type;
+ in
+ concat
+ (map make_header_field
+ (("Status", concat [code, " ", reason])
+ :: (the_list o Option.map show_content_type) content_type
+ @ extra_fields)
+ @ [crlf])
+ end;
+
+val split_fields = Substring.splitl (fn c => c <> #"=")
+ #> apsnd (Substring.triml 1);
+
+fun decode_url s =
+ let
+ fun to_char c =
+ Substring.triml 1 c
+ |> Int.scan StringCvt.HEX Substring.getc
+ |> the
+ |> fst
+ |> Char.chr
+ |> String.str
+ |> Substring.full
+ handle Option => c;
+
+ fun f (done, s) =
+ let
+ val (pre, post) = Substring.splitl (Char.notContains "+%") s;
+ in
+ if Substring.isEmpty post
+ then (Substring.concat o rev) (pre::done)
+ else
+ if Substring.first post = SOME #"+"
+ (* Substring.isPrefix "+" post *)(* seg fault in Poly/ML 5.1 *)
+ then f (Substring.full " "::pre::done, Substring.triml 1 post)
+ else let
+ val (c, rest) = Substring.splitAt (post, 3)
+ handle Subscript =>
+ (Substring.full "%25", Substring.triml 1 post);
+ in f (to_char c::pre::done, rest) end
+ end;
+ in f ([], s) end;
+
+val parse_query_string =
+ Substring.full
+ #> Substring.tokens (Char.contains "&;")
+ #> map split_fields
+ #> map (pairself (UnicodeSymbols.utf8_to_symbols o decode_url))
+ #> distinct ((op =) o pairself fst)
+ #> Symtab.make;
+
+local
+fun to_entity #" " = "+"
+ | to_entity c =
+ if Char.isAlphaNum c orelse Char.contains ".-~_" c
+ then String.str c
+ else "%" ^ Int.fmt StringCvt.HEX (Char.ord c);
+in
+val encode_url = Substring.translate to_entity o Substring.full;
+end
+
+fun join_pairs (n, v) = encode_url n ^ "=" ^ encode_url v;
+
+val make_query_string =
+ Symtab.dest
+ #> map join_pairs
+ #> String.concatWith "&";
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,135 @@
+#!/usr/bin/env bash
+#
+# Author: Timothy Bourke, NICTA
+# Based on scripts by Makarius Wenzel, TU Muenchen
+#
+# DESCRIPTION: run find theorems web server
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: $ISABELLE_TOOL $PRG [Command] [Options] [HEAP]"
+ echo
+ echo " Command must be one of:"
+ echo " start start lighttpd and isabelle"
+ echo " stop stop lighttpd and isabelle"
+ echo " status show www and scgi port statuses"
+ echo
+ echo " Options are:"
+ echo " -l make log file"
+ echo " -c specify lighttpd config file"
+ echo " (default: $WWWCONFIG)"
+ echo
+ echo " Provide a web interface to find_theorems against the given HEAP"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+function kill_by_port () {
+ IPADDR='[0-9]*\.[0-9]*\.[0-9]*\.[0-9]*'
+ PID=$(netstat -nltp 2>/dev/null \
+ | sed -ne "s#^.*${IPADDR}:$1 *${IPADDR}:.*LISTEN *\([0-9]*\)/.*#\1#p")
+ if [ "$PID" != "" ]; then
+ kill -9 $PID
+ fi
+}
+
+function show_socket_status () {
+ netstat -latp 2>/dev/null | grep ":$1 "
+}
+
+## process command line
+
+case "$1" in
+ start|stop|status)
+ COMMAND="$1"
+ ;;
+ *)
+ usage
+ ;;
+esac
+
+shift
+
+# options
+
+NO_OPTS=true
+LOGFILE=false
+
+while getopts "lc:" OPT
+do
+ NO_OPTS=""
+ case "$OPT" in
+ l)
+ LOGFILE=true
+ ;;
+ c)
+ USER_CONFIG="$OPTARG"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+# args
+
+INPUT=""
+
+if [ "$#" -ge 1 ]; then
+ INPUT="$1"
+ shift
+fi
+
+[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+
+[ -x "$LIGHTTPD" ] || fail "lighttpd not found at $LIGHTTPD"
+
+if [ -n "$USER_CONFIG" ]; then
+ WWWCONFIG="$USER_CONFIG"
+else
+ TMP=$(mktemp "/tmp/lighttpd.conf.$$.XXX")
+ echo "server.document-root = \"$WWWFINDDIR/www\"" > "$TMP"
+ cat "$WWWCONFIG" >> "$TMP"
+ WWWCONFIG="$TMP"
+fi
+
+
+## main
+
+WWWPORT=`sed -e 's/[ ]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
+SCGIPORT=`sed -e 's/[ ]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
+MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
+
+case "$COMMAND" in
+ start)
+ "$LIGHTTPD" -f "$WWWCONFIG"
+ if [ "$LOGFILE" = true ]; then
+ (cd "$WWWFINDDIR"; \
+ nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" "$INPUT") &
+ else
+ (cd "$WWWFINDDIR"; \
+ nohup "$ISABELLE_PROCESS" -r -u -e "$MLSTARTSERVER" \
+ "$INPUT" > /dev/null 2> /dev/null) &
+ fi
+ ;;
+ stop)
+ kill_by_port $SCGIPORT
+ kill_by_port $WWWPORT
+ ;;
+ status)
+ show_socket_status $WWWPORT
+ show_socket_status $SCGIPORT
+ ;;
+esac
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/lighttpd.conf Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,20 @@
+server.port = 8000
+
+# debug.log-request-header = "enable"
+# debug.log-file-not-found = "enable"
+# debug.log-request-handling = "enable"
+# debug.log-response-header = "enable"
+
+mimetype.assign = (
+ ".html" => "text/html; charset=UTF-8",
+ ".css" => "text/css; charset=UTF-8",
+)
+
+server.modules = ( "mod_scgi" )
+
+scgi.server = ("/isabelle" => ((
+ "host" => "127.0.0.1",
+ "port" => 64000,
+ "check-local" => "disable"
+ )))
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/mime.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,56 @@
+(* Title: mime_types.ML
+ Author: Timothy Bourke, NICTA
+
+Rudimentary support for mime_types.
+*)
+
+signature MIME =
+sig
+ datatype t = Type of {
+ main : string,
+ sub : string,
+ params : (string * string) list
+ }
+
+ val plain : t
+ val html : t
+
+ val parse_type : string -> t option
+ val show_type : t -> string
+end;
+
+structure Mime: MIME =
+struct
+
+datatype t = Type of {
+ main : string,
+ sub : string,
+ params : (string * string) list
+ };
+
+val strip =
+ Substring.dropl Char.isSpace
+ #> Substring.dropr Char.isSpace;
+
+val split_fields =
+ Substring.splitl (fn c => c <> #"=")
+ #> apsnd (Substring.triml 1)
+ #> pairself (Substring.string o strip);
+
+fun show_param (n, v) = concat ["; ", n, "=", v];
+
+fun show_type (Type {main, sub, params}) =
+ concat ([main, "/", sub] @ map show_param params);
+
+fun parse_type s =
+ (case Substring.fields (Char.contains "/;") (Substring.full s) of
+ t::s::ps => SOME (Type { main = (Substring.string o strip) t,
+ sub = (Substring.string o strip) s,
+ params = map split_fields ps })
+ | _ => NONE);
+
+val plain = the (parse_type "text/plain; charset=utf-8");
+val html = the (parse_type "text/html; charset=utf-8");
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/scgi_req.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,160 @@
+(* Title: parse_scgi_req.ML
+ Author: Timothy Bourke, NICTA
+
+Parses an SCGI (Simple Common Gateway Interface) header.
+See: http://python.ca/scgi/protocol.txt
+*)
+
+signature SCGI_REQ =
+sig
+ exception InvalidReq of string
+
+ datatype req_method = Get | Head | Post
+
+ datatype t = Req of {
+ path_info : string,
+ path_translated : string,
+ script_name : string,
+ request_method : req_method,
+ query_string : string Symtab.table,
+ content_type : Mime.t option,
+ environment : Word8VectorSlice.slice Symtab.table
+ }
+
+ val parse : BinIO.instream -> t * (BinIO.instream * int)
+ val test : string -> unit
+
+ val show : t -> string
+end;
+
+structure ScgiReq : SCGI_REQ =
+struct
+
+exception InvalidReq of string;
+
+datatype req_method = Get | Head | Post;
+
+datatype t = Req of {
+ path_info : string,
+ path_translated : string,
+ script_name : string,
+ request_method : req_method,
+ query_string : string Symtab.table,
+ content_type : Mime.t option,
+ environment : Word8VectorSlice.slice Symtab.table
+ };
+
+fun parse_req_method "POST" = Post
+ | parse_req_method "HEAD" = Head
+ | parse_req_method _ = Get;
+
+fun show_req_method Get = "Get"
+ | show_req_method Post = "Post"
+ | show_req_method Head = "Head";
+
+fun find_nulls (idx, 0wx00, idxs) = idx::idxs
+ | find_nulls (_, _, idxs) = idxs;
+
+fun read_net_string fin =
+ let
+ fun read_size (_, NONE) = raise InvalidReq "Bad netstring length."
+ | read_size (t, SOME 0wx3a) = t
+ | read_size (t, SOME d) =
+ let
+ val n = (Word8.toInt d) - 0x30;
+ in
+ if n >=0 andalso n <= 9
+ then read_size (t * 10 + n, BinIO.input1 fin)
+ else read_size (t, NONE)
+ end;
+ val size = read_size (0, BinIO.input1 fin);
+ val payload = BinIO.inputN (fin, size);
+ in
+ (case (Word8Vector.length payload = size, BinIO.input1 fin) of
+ (true, SOME 0wx2c) => payload
+ | _ => raise InvalidReq "Bad netstring.")
+ end;
+
+fun split_fields vec =
+ let
+ val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
+
+ fun pr NONE = "NONE"
+ | pr (SOME i) = "SOME " ^ Int.toString i;
+
+ fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
+ | hd_diff _ = NONE;
+
+ fun slice [] = []
+ | slice (idxs as idx::idxs') =
+ Word8VectorSlice.slice (vec, idx + 1, hd_diff idxs) :: slice idxs';
+
+ fun make_pairs (x::y::xys) = (Byte.unpackStringVec x, y) :: make_pairs xys
+ | make_pairs _ = [];
+
+ in make_pairs (slice nulls) end;
+
+fun parse fin =
+ let
+ val raw_fields = read_net_string fin;
+ val fields = split_fields raw_fields;
+ val env = Symtab.make fields;
+
+ fun field name =
+ (case Symtab.lookup env name of
+ NONE => ""
+ | SOME wv => Byte.unpackStringVec wv);
+
+ val content_length =
+ (the o Int.fromString o field) "CONTENT_LENGTH"
+ handle _ => raise InvalidReq "Bad CONTENT_LENGTH";
+
+ val req = Req {
+ path_info = field "PATH_INFO",
+ path_translated = field "PATH_TRANSLATED",
+ script_name = field "SCRIPT_NAME",
+ request_method = (parse_req_method o field) "REQUEST_METHOD",
+ query_string = (HttpUtil.parse_query_string o field) "QUERY_STRING",
+ content_type = (Mime.parse_type o field) "CONTENT_TYPE",
+ environment = env
+ }
+
+ in (req, (fin, content_length)) end;
+
+fun show (Req {path_info, path_translated, script_name,
+ request_method, query_string, content_type, environment}) =
+ let
+ fun show_symtab to_string table = let
+ fun show (n, v) r = ["\t", n, " = \"", to_string v, "\"\n"] @ r;
+ in Symtab.fold show table [] end;
+ in
+ concat
+ (["path_info: \"", path_info, "\"\n",
+ "path_translated: \"", path_translated, "\"\n",
+ "script_name: \"", script_name, "\"\n",
+ "request_method: \"", show_req_method request_method, "\"\n",
+ "query_string:\n"]
+ @
+ show_symtab I query_string
+ @
+ ["content_type: ",
+ (the_default "" o Option.map Mime.show_type) content_type, "\n",
+ "environment:\n"]
+ @
+ show_symtab Byte.unpackStringVec environment)
+ end;
+
+fun test path =
+ let
+ val fin = BinIO.openIn path;
+ val (req, cs) = parse fin;
+ val () = TextIO.print (show req);
+ val () =
+ BinIO.inputN cs
+ |> Word8VectorSlice.full
+ |> Byte.unpackStringVec
+ |> TextIO.print;
+ in BinIO.closeIn fin end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/scgi_server.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,125 @@
+(* Title: scgi_echo.ML
+ Author: Timothy Bourke, NICTA
+
+Simple SCGI server.
+*)
+
+signature SCGI_SERVER =
+sig
+ val max_threads : int Unsynchronized.ref
+ type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit
+ val register : (string * Mime.t option * handler) -> unit
+ val server : string -> int -> unit
+ val server' : int -> string -> int -> unit (* keeps trying for port *)
+end;
+
+structure ScgiServer : SCGI_SERVER =
+struct
+val max_threads = Unsynchronized.ref 5;
+
+type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit;
+
+local
+val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table);
+in
+fun register (name, mime, f) =
+ Unsynchronized.change servers (Symtab.update_new (name, (mime, f)));
+fun lookup name = Symtab.lookup (!servers) name;
+
+fun dump_handlers () = (
+ tracing(" with handlers:");
+ app (fn (x, _) => tracing (" - " ^ x)) (Symtab.dest (!servers)))
+end;
+
+fun server server_prefix port =
+ let
+ val passive_sock = SocketUtil.init_server_socket (SOME "localhost") port;
+
+ val thread_wait = ConditionVar.conditionVar ();
+ val thread_wait_mutex = Mutex.mutex ();
+
+ local
+ val threads = Unsynchronized.ref ([] : Thread.thread list);
+ fun purge () = Unsynchronized.change threads (filter Thread.isActive);
+ in
+ fun add_thread th = Unsynchronized.change threads (cons th);
+
+ fun launch_thread threadf =
+ (purge ();
+ if length (!threads) < (!max_threads) then ()
+ else (tracing ("Waiting for a free thread...");
+ ConditionVar.wait (thread_wait, thread_wait_mutex));
+ add_thread
+ (Thread.fork
+ (fn () => exception_trace threadf,
+ [Thread.EnableBroadcastInterrupt true,
+ Thread.InterruptState
+ Thread.InterruptAsynchOnce])))
+ end;
+
+ fun loop () =
+ let
+ val (sock, _)= Socket.accept passive_sock;
+
+ val (sin, sout) = SocketUtil.make_streams sock;
+
+ fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
+ fun send_log msg = (tracing msg; send msg);
+
+ fun get_content (st, 0) = Word8Vector.fromList []
+ | get_content x = BinIO.inputN x;
+
+ fun do_req () =
+ let
+ val (req as ScgiReq.Req {path_info, request_method, ...},
+ content_is) =
+ ScgiReq.parse sin
+ handle ScgiReq.InvalidReq s =>
+ (send
+ (HttpUtil.reply_header (HttpStatus.bad_request, NONE, []));
+ raise Fail ("Invalid request: " ^ s));
+ val () = tracing ("request: " ^ path_info);
+ in
+ (case lookup (unprefix server_prefix path_info) of
+ NONE => send (HttpUtil.reply_header (HttpStatus.not_found, NONE, []))
+ | SOME (NONE, f) => f (req, get_content content_is, send)
+ | SOME (t, f) =>
+ (send (HttpUtil.reply_header (HttpStatus.ok, t, []));
+ if request_method = ScgiReq.Head then ()
+ else f (req, get_content content_is, send)))
+ end;
+
+ fun thread_req () =
+ (do_req () handle e => (warning (exnMessage e));
+ BinIO.closeOut sout handle e => warning (exnMessage e);
+ BinIO.closeIn sin handle e => warning (exnMessage e);
+ Socket.close sock handle e => warning (exnMessage e);
+ tracing ("request done.");
+ ConditionVar.signal thread_wait);
+ in
+ launch_thread thread_req;
+ loop ()
+ end;
+ in
+ tracing ("SCGI server started.");
+ dump_handlers ();
+ loop ();
+ Socket.close passive_sock
+ end;
+
+local
+val delay = 5;
+in
+fun server' 0 server_prefix port = (warning "Giving up."; exit 1)
+ | server' countdown server_prefix port =
+ server server_prefix port
+ handle OS.SysErr ("bind failed", _) =>
+ (warning ("Could not acquire port "
+ ^ Int.toString port ^ ". Trying again in "
+ ^ Int.toString delay ^ " seconds...");
+ OS.Process.sleep (Time.fromSeconds delay);
+ server' (countdown - 1) server_prefix port);
+end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/socket_util.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,94 @@
+(* Title: socket_util.ML
+ Author: Emden R. Gansner and John H. Reppy
+ SML Basis Library, section 10
+
+Routines for working with sockets.
+*)
+
+signature SOCKET_UTIL =
+sig
+ val init_server_socket : string option -> int ->
+ Socket.passive INetSock.stream_sock
+
+ val make_streams : Socket.active INetSock.stream_sock
+ -> BinIO.instream * BinIO.outstream
+end;
+
+structure SocketUtil =
+struct
+
+fun init_server_socket hosto port =
+ let
+ val sock = INetSock.TCP.socket ();
+ val addr =
+ (case hosto of
+ NONE => INetSock.any port
+ | SOME host =>
+ NetHostDB.getByName host
+ |> the
+ |> NetHostDB.addr
+ |> rpair port
+ |> INetSock.toAddr
+ handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
+ in
+ Socket.bind (sock, addr);
+ Socket.listen (sock, 5);
+ sock
+ end;
+
+fun make_streams sock =
+ let
+ val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
+
+ val sock_name =
+ String.concat [ NetHostDB.toString haddr, ":", Int.toString port ];
+
+ val rd =
+ BinPrimIO.RD {
+ name = sock_name,
+ chunkSize = Socket.Ctl.getRCVBUF sock,
+ readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
+ readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
+ readVecNB = NONE,
+ readArrNB = NONE,
+ block = NONE,
+ canInput = NONE,
+ avail = fn () => NONE,
+ getPos = NONE,
+ setPos = NONE,
+ endPos = NONE,
+ verifyPos = NONE,
+ close = fn () => Socket.close sock,
+ ioDesc = NONE
+ };
+
+ val wr =
+ BinPrimIO.WR {
+ name = sock_name,
+ chunkSize = Socket.Ctl.getSNDBUF sock,
+ writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
+ writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
+ writeVecNB = NONE,
+ writeArrNB = NONE,
+ block = NONE,
+ canOutput = NONE,
+ getPos = NONE,
+ setPos = NONE,
+ endPos = NONE,
+ verifyPos = NONE,
+ close = fn () => Socket.close sock,
+ ioDesc = NONE
+ };
+
+ val in_strm =
+ BinIO.mkInstream (
+ BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
+
+ val out_strm =
+ BinIO.mkOutstream (
+ BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
+
+ in (in_strm, out_strm) end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,277 @@
+(* Title: Pure/Thy/unicode_symbols.ML
+ Author: Timothy Bourke, NICTA
+
+Parse the etc/symbols file.
+*)
+
+signature UNICODE_SYMBOLS =
+sig
+val symbol_to_unicode : string -> int option
+val abbrev_to_unicode : string -> int option
+val unicode_to_symbol : int -> string option
+val unicode_to_abbrev : int -> string option
+val utf8_to_symbols : string -> string
+val utf8 : int list -> string
+end;
+
+structure UnicodeSymbols (*: UNICODE_SYMBOLS*) =
+struct
+
+local (* Lexer *)
+
+open Basic_Symbol_Pos
+
+val keywords =
+ Scan.make_lexicon (map Symbol.explode ["code", "font", "abbrev", ":"]);
+
+datatype token_kind =
+ Symbol | AsciiSymbol | Keyword | Name | Code | Space | Comment | EOF;
+
+datatype token = Token of token_kind * string * Position.range;
+
+fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
+
+in
+
+fun mk_eof pos = Token (EOF, "", (pos, Position.none));
+
+fun str_of_token (Token (_, s, _)) = s;
+
+fun pos_of_token (Token (_, _, (pos, _))) = pos;
+
+fun int_of_code (Token (Code, s, _)) = #value (Lexicon.read_xnum s)
+ | int_of_code _ = error "internal error in UnicodeSymbols.int_of_code"
+
+fun is_proper (Token (Space, _, _)) = false
+ | is_proper (Token (Comment, _, _)) = false
+ | is_proper _ = true;
+
+fun is_keyword kw (Token (Keyword, kw', _)) = (kw = kw')
+ | is_keyword _ _ = false;
+
+fun is_ascii_sym (Token (AsciiSymbol, _, _)) = true
+ | is_ascii_sym _ = false;
+
+fun is_hex_code (Token (Code, _, _)) = true
+ | is_hex_code _ = false;
+
+fun is_symbol (Token (Symbol, _, _)) = true
+ | is_symbol _ = false;
+
+fun is_name (Token (Name, _, _)) = true
+ | is_name _ = false;
+
+fun is_eof (Token (EOF, _, _)) = true
+ | is_eof _ = false;
+
+fun end_position_of (Token (_, _, (_, epos))) = epos;
+
+val is_space = symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
+val scan_space =
+ (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
+ ||
+ Scan.many is_space @@@ ($$$ "\n")) >> token Space;
+
+val scan_code = Lexicon.scan_hex #>> token Code;
+
+val scan_ascii_symbol = Scan.one
+ ((fn x => Symbol.is_ascii x andalso
+ not (Symbol.is_ascii_letter x
+ orelse Symbol.is_ascii_digit x
+ orelse Symbol.is_ascii_blank x)) o symbol)
+ -- Scan.many (not o Symbol.is_ascii_blank o symbol)
+ >> (token AsciiSymbol o op ::);
+
+fun not_contains xs c = not ((symbol c) mem_string (explode xs));
+val scan_comment =
+ $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
+ >> token Comment;
+
+fun tokenize syms =
+ let
+ val scanner =
+ Scan.one (Symbol.is_symbolic o symbol) >> (token Symbol o single) ||
+ scan_comment ||
+ scan_space ||
+ scan_code ||
+ Scan.literal keywords >> token Keyword ||
+ scan_ascii_symbol ||
+ Lexicon.scan_id >> token Name;
+ val scan_token = Symbol_Pos.!!! "Lexical error" (Scan.bulk scanner);
+ in
+ (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
+ (toks, []) => toks
+ | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss
+ ^ Position.str_of (#1 (Symbol_Pos.range ss))))
+ end;
+
+val stopper =
+ Scan.stopper
+ (fn [] => mk_eof Position.none
+ | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+
+end;
+
+local (* Parser *)
+
+structure P = OuterParse;
+
+fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
+val hex_code = Scan.one is_hex_code >> int_of_code;
+val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
+val symbol = Scan.one is_symbol >> (fn t => (str_of_token t, pos_of_token t));
+val name = Scan.one is_name >> str_of_token;
+
+val unicode = $$$ "code" -- $$$ ":" |-- hex_code;
+val font = Scan.option ($$$ "font" -- $$$ ":" |-- name);
+val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
+ |-- (ascii_sym || $$$ ":" || name));
+
+in
+
+val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
+
+val symbols_path =
+ [getenv "ISABELLE_HOME", "etc", "symbols"]
+ |> map Path.explode
+ |> Path.appends;
+
+end;
+
+local (* build tables *)
+
+fun add_entries ((fromsym, fromabbr, tosym, toabbr), ((sym, pos), uni, oabbr)) =
+ (case oabbr of
+ NONE =>
+ (Symtab.update_new (sym, uni) fromsym,
+ fromabbr,
+ Inttab.update (uni, sym) tosym,
+ toabbr)
+ | SOME abbr =>
+ (Symtab.update_new (sym, uni) fromsym,
+ Symtab.update_new (abbr, uni) fromabbr,
+ Inttab.update (uni, sym) tosym,
+ Inttab.update (uni, abbr) toabbr))
+ handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos)
+ | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos);
+
+in
+
+fun read_symbols path =
+ let
+ val parsed_lines =
+ File.read path
+ |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
+ |> tokenize
+ |> filter is_proper
+ |> Scan.finite stopper (Scan.repeat line)
+ |> fst;
+ in
+ Library.foldl add_entries
+ ((Symtab.empty, Symtab.empty, Inttab.empty, Inttab.empty),
+ parsed_lines)
+ end;
+
+end;
+
+local
+val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
+in
+val symbol_to_unicode = Symtab.lookup fromsym;
+val abbrev_to_unicode = Symtab.lookup fromabbr;
+val unicode_to_symbol = Inttab.lookup tosym;
+val unicode_to_abbrev = Inttab.lookup toabbr;
+end;
+
+fun utf8_to_symbols utf8str =
+ let
+ val get_next =
+ Substring.getc
+ #> Option.map (apfst Byte.charToByte);
+ val wstr = String.str o Byte.byteToChar;
+ val replacement_char = "\<questiondown>";
+
+ fun word_to_symbol w =
+ (case (unicode_to_symbol o Word32.toInt) w of
+ NONE => "?"
+ | SOME s => s);
+
+ fun andb32 (w1, w2) =
+ Word8.andb(w1, w2)
+ |> Word8.toLarge
+ |> Word32.fromLarge;
+
+ fun read_next (ss, 0, c) = (word_to_symbol c, ss)
+ | read_next (ss, n, c) =
+ (case get_next ss of
+ NONE => (replacement_char, ss)
+ | SOME (w, ss') =>
+ if Word8.andb (w, 0wxc0) <> 0wx80
+ then (replacement_char, ss')
+ else
+ let
+ val w' = (Word8.andb (w, 0wx3f));
+ val bw = (Word32.fromLarge o Word8.toLarge) w';
+ val c' = Word32.<< (c, 0wx6);
+ in read_next (ss', n - 1, Word32.orb (c', bw)) end);
+
+ fun do_char (w, ss) =
+ if Word8.andb (w, 0wx80) = 0wx00
+ then (wstr w, ss)
+ else if Word8.andb (w, 0wx60) = 0wx40
+ then read_next (ss, 1, andb32 (w, 0wx1f))
+ else if Word8.andb (w, 0wxf0) = 0wxe0
+ then read_next (ss, 2, andb32 (w, 0wx0f))
+ else if Word8.andb (w, 0wxf8) = 0wxf0
+ then read_next (ss, 3, andb32 (w, 0wx07))
+ else (replacement_char, ss);
+
+ fun read (rs, ss) =
+ (case Option.map do_char (get_next ss) of
+ NONE => (implode o rev) rs
+ | SOME (s, ss') => read (s::rs, ss'));
+ in read ([], Substring.full utf8str) end;
+
+local
+
+fun consec n =
+ fn w => (
+ Word32.>> (w, Word.fromInt (n * 6))
+ |> (curry Word32.andb) 0wx3f
+ |> (curry Word32.orb) 0wx80
+ |> Word8.fromLargeWord o Word32.toLargeWord);
+
+fun stamp n =
+ fn w => (
+ Word32.>> (w, Word.fromInt (n * 6))
+ |> (curry Word32.andb) (Word32.>> (0wx000000ff, Word.fromInt (n + 2)))
+ |> (curry Word32.orb) (Word32.<< (0wxffffffff, Word.fromInt (7 - n)))
+ |> Word8.fromLargeWord o Word32.toLargeWord);
+
+fun to_utf8_bytes i =
+ if i <= 0x007f
+ then [Word8.fromInt i]
+ else let
+ val w = Word32.fromInt i;
+ in
+ if i < 0x07ff
+ then [stamp 1 w, consec 0 w]
+ else if i < 0xffff
+ then [stamp 2 w, consec 1 w, consec 0 w]
+ else if i < 0x10ffff
+ then [stamp 3 w, consec 2 w, consec 1 w, consec 0 w]
+ else []
+ end;
+
+in
+
+fun utf8 is =
+ map to_utf8_bytes is
+ |> flat
+ |> Word8Vector.fromList
+ |> Byte.bytesToString;
+
+end
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/www/basic.css Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,109 @@
+
+body {
+ font-family: sans-serif;
+ background-color: white;
+}
+
+p.error {
+ font-weight: bold;
+ color: #ff0000;
+}
+
+p.info {
+ font-style: italic;
+}
+
+input#query {
+ width: 100%;
+}
+
+legend {
+ padding : 0.5em;
+ font-weight: bold;
+}
+
+label {
+ width: 8em;
+ float: left;
+}
+
+fieldset {
+ padding: 0 1em 1em 1em;
+}
+
+div.settings {
+ padding-top: 2em;
+ float: left;
+}
+
+div.settings label {
+ font-style: italic;
+}
+
+div.settings div {
+ padding-top: 1ex;
+}
+
+div.mainbuttons {
+ margin-top: 8.5ex;
+ float: right
+}
+
+div.mainbuttons #reset {
+ margin-right: 5em;
+}
+
+table.findtheorems {
+ width: 100%;
+ padding-top: 1em;
+ padding-bottom: 2em;
+}
+
+table.findtheorems tr.row0 { background-color: white; }
+table.findtheorems tr.row1 { background-color: #f5f5f5; }
+table.findtheorems tbody tr:hover { background-color: #dcdcdc; }
+
+table.findtheorems td {
+ vertical-align: top;
+ padding-left: 1em;
+ padding-bottom: 1em;
+}
+
+table.findtheorems td.name {
+ font-size: small;
+ font-style: italic;
+ padding-right: 1em;
+}
+table.findtheorems td.thm {
+ vertical-align: top;
+ font-size: small;
+}
+table.findtheorems td.thm pre {
+ margin: 0em;
+}
+table.findtheorems th {
+ text-align: left;
+ padding-bottom: 1ex;
+}
+
+table.findtheoremsquery th {
+ font-weight: normal;
+ text-align: left;
+ padding-top: 1em;
+}
+
+span.class { color: #ff0000 }
+span.tfree { color: #9370d8 }
+span.tvar { color: #9370d8 }
+span.free { color: #add8e6 }
+span.bound { color: #008400 }
+span.var { color: #00008b }
+span.xstr { color: #000000 }
+
+span.sorried:after { content: " [!]"; }
+
+div.help a {
+ font-size: xx-small;
+ color: #d3d3d3;
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/www/find_theorems.js Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,410 @@
+/* $Id$
+ * Author: Timothy Bourke, NICTA
+ */
+var utf8 = new Object();
+utf8['\\<supseteq>'] = 'โ';
+utf8['\\<KK>'] = '๐';
+utf8['\\<up>'] = 'โ';
+utf8['\\<otimes>'] = 'โ';
+utf8['\\<aa>'] = '๐';
+utf8['\\<dagger>'] = 'โ ';
+utf8['\\<frown>'] = 'โข';
+utf8['\\<guillemotleft>'] = 'ยซ';
+utf8['\\<qq>'] = '๐ฎ';
+utf8['\\<X>'] = '๐ณ';
+utf8['\\<triangleright>'] = 'โน';
+utf8['\\<guillemotright>'] = 'ยป';
+utf8['\\<nu>'] = 'ฮฝ';
+utf8['\\<sim>'] = 'โผ';
+utf8['\\<rightharpoondown>'] = 'โ';
+utf8['\\<p>'] = '๐';
+utf8['\\<Up>'] = 'โ';
+utf8['\\<triangleq>'] = 'โ';
+utf8['\\<nine>'] = '๐ต';
+utf8['\\<preceq>'] = 'โผ';
+utf8['\\<nabla>'] = 'โ';
+utf8['\\<FF>'] = '๐';
+utf8['\\<Im>'] = 'โ';
+utf8['\\<VV>'] = '๐';
+utf8['\\<spacespace>'] = 'โฃ';
+utf8['\\<and>'] = 'โง';
+utf8['\\<mapsto>'] = 'โฆ';
+utf8['\\<ll>'] = '๐ฉ';
+utf8['\\<F>'] = 'โฑ';
+utf8['\\<degree>'] = 'ยฐ';
+utf8['\\<beta>'] = 'ฮฒ';
+utf8['\\<Colon>'] = 'โท';
+utf8['\\<bool>'] = '๐น';
+utf8['\\<e>'] = '๐พ';
+utf8['\\<lozenge>'] = 'โ';
+utf8['\\<u>'] = '๐';
+utf8['\\<sharp>'] = 'โฏ';
+utf8['\\<Longleftrightarrow>'] = 'โบ';
+utf8['\\<Otimes>'] = 'โจ';
+utf8['\\<EE>'] = '๐';
+utf8['\\<I>'] = 'โ';
+utf8['\\<UU>'] = '๐';
+utf8['\\<exclamdown>'] = 'ยก';
+utf8['\\<dots>'] = 'โฆ';
+utf8['\\<N>'] = '๐ฉ';
+utf8['\\<kk>'] = '๐จ';
+utf8['\\<plusminus>'] = 'ยฑ';
+utf8['\\<E>'] = 'โฐ';
+utf8['\\<triangle>'] = 'โณ';
+utf8['\\<eta>'] = 'ฮท';
+utf8['\\<triangleleft>'] = 'โ';
+utf8['\\<chi>'] = 'ฯ';
+utf8['\\<z>'] = '๐';
+utf8['\\<hungarumlaut>'] = 'ห';
+utf8['\\<partial>'] = 'โ';
+utf8['\\<three>'] = '๐ฏ';
+utf8['\\<lesssim>'] = 'โฒ';
+utf8['\\<subset>'] = 'โ';
+utf8['\\<H>'] = 'โ';
+utf8['\\<leftarrow>'] = 'โ';
+utf8['\\<PP>'] = '๐';
+utf8['\\<sqsupseteq>'] = 'โ';
+utf8['\\<R>'] = 'โ';
+utf8['\\<bowtie>'] = 'โจ';
+utf8['\\<C>'] = '๐';
+utf8['\\<ddagger>'] = 'โก';
+utf8['\\<ff>'] = '๐ฃ';
+utf8['\\<turnstile>'] = 'โข';
+utf8['\\<bar>'] = 'ยฆ';
+utf8['\\<propto>'] = 'โ';
+utf8['\\<S>'] = '๐ฎ';
+utf8['\\<vv>'] = '๐ณ';
+utf8['\\<lhd>'] = 'โฒ';
+utf8['\\<paragraph>'] = 'ยถ';
+utf8['\\<mu>'] = 'ฮผ';
+utf8['\\<rightharpoonup>'] = 'โ';
+utf8['\\<Inter>'] = 'โ';
+utf8['\\<o>'] = '๐';
+utf8['\\<asymp>'] = 'โ';
+utf8['\\<Leftarrow>'] = 'โ';
+utf8['\\<Sqinter>'] = 'โจ
';
+utf8['\\<eight>'] = '๐ด';
+utf8['\\<succeq>'] = 'โฝ';
+utf8['\\<forall>'] = 'โ';
+utf8['\\<complex>'] = 'โ';
+utf8['\\<GG>'] = '๐';
+utf8['\\<Coprod>'] = 'โ';
+utf8['\\<L>'] = 'โ';
+utf8['\\<WW>'] = '๐';
+utf8['\\<leadsto>'] = 'โ';
+utf8['\\<D>'] = '๐';
+utf8['\\<angle>'] = 'โ ';
+utf8['\\<section>'] = 'ยง';
+utf8['\\<TTurnstile>'] = 'โซ';
+utf8['\\<mm>'] = '๐ช';
+utf8['\\<T>'] = '๐ฏ';
+utf8['\\<alpha>'] = 'ฮฑ';
+utf8['\\<leftharpoondown>'] = 'โฝ';
+utf8['\\<rho>'] = 'ฯ';
+utf8['\\<wrong>'] = 'โ';
+utf8['\\<l>'] = '๐
';
+utf8['\\<doteq>'] = 'โ';
+utf8['\\<times>'] = 'ร';
+utf8['\\<noteq>'] = 'โ ';
+utf8['\\<rangle>'] = 'โฉ';
+utf8['\\<div>'] = 'รท';
+utf8['\\<Longrightarrow>'] = 'โน';
+utf8['\\<BB>'] = '๐
';
+utf8['\\<sqsupset>'] = 'โ';
+utf8['\\<rightarrow>'] = 'โ';
+utf8['\\<real>'] = 'โ';
+utf8['\\<hh>'] = '๐ฅ';
+utf8['\\<Phi>'] = 'ฮฆ';
+utf8['\\<integral>'] = 'โซ';
+utf8['\\<CC>'] = 'โญ';
+utf8['\\<euro>'] = 'โฌ';
+utf8['\\<xx>'] = '๐ต';
+utf8['\\<Y>'] = '๐ด';
+utf8['\\<zeta>'] = 'ฮถ';
+utf8['\\<longleftarrow>'] = 'โต';
+utf8['\\<a>'] = '๐บ';
+utf8['\\<onequarter>'] = 'ยผ';
+utf8['\\<And>'] = 'โ';
+utf8['\\<downharpoonright>'] = 'โ';
+utf8['\\<phi>'] = 'ฯ';
+utf8['\\<q>'] = '๐';
+utf8['\\<Rightarrow>'] = 'โ';
+utf8['\\<clubsuit>'] = 'โฃ';
+utf8['\\<ggreater>'] = 'โซ';
+utf8['\\<two>'] = '๐ฎ';
+utf8['\\<succ>'] = 'โป';
+utf8['\\<AA>'] = '๐';
+utf8['\\<lparr>'] = 'โฆ';
+utf8['\\<Squnion>'] = 'โจ';
+utf8['\\<HH>'] = 'โ';
+utf8['\\<sqsubseteq>'] = 'โ';
+utf8['\\<QQ>'] = '๐';
+utf8['\\<setminus>'] = 'โ';
+utf8['\\<Lambda>'] = 'ฮ';
+utf8['\\<Re>'] = 'โ';
+utf8['\\<J>'] = '๐ฅ';
+utf8['\\<gg>'] = '๐ค';
+utf8['\\<hyphen>'] = 'ยญ';
+utf8['\\<B>'] = 'โฌ';
+utf8['\\<Z>'] = '๐ต';
+utf8['\\<ww>'] = '๐ด';
+utf8['\\<lambda>'] = 'ฮป';
+utf8['\\<onehalf>'] = 'ยฝ';
+utf8['\\<f>'] = '๐ฟ';
+utf8['\\<Or>'] = 'โ';
+utf8['\\<v>'] = '๐';
+utf8['\\<natural>'] = 'โฎ';
+utf8['\\<seven>'] = '๐ณ';
+utf8['\\<Oplus>'] = 'โจ';
+utf8['\\<subseteq>'] = 'โ';
+utf8['\\<rfloor>'] = 'โ';
+utf8['\\<LL>'] = '๐';
+utf8['\\<Sum>'] = 'โ';
+utf8['\\<ominus>'] = 'โ';
+utf8['\\<bb>'] = '๐';
+utf8['\\<Pi>'] = 'ฮ ';
+utf8['\\<cent>'] = 'ยข';
+utf8['\\<diamond>'] = 'โ';
+utf8['\\<mho>'] = 'โง';
+utf8['\\<O>'] = '๐ช';
+utf8['\\<rr>'] = '๐ฏ';
+utf8['\\<twosuperior>'] = 'ยฒ';
+utf8['\\<leftharpoonup>'] = 'โผ';
+utf8['\\<pi>'] = 'ฯ';
+utf8['\\<k>'] = '๐';
+utf8['\\<star>'] = 'โ';
+utf8['\\<rightleftharpoons>'] = 'โ';
+utf8['\\<equiv>'] = 'โก';
+utf8['\\<langle>'] = 'โจ';
+utf8['\\<Longleftarrow>'] = 'โธ';
+utf8['\\<nexists>'] = 'โ';
+utf8['\\<Odot>'] = 'โจ';
+utf8['\\<lfloor>'] = 'โ';
+utf8['\\<sqsubset>'] = 'โ';
+utf8['\\<SS>'] = '๐';
+utf8['\\<box>'] = 'โก';
+utf8['\\<index>'] = 'ฤฑ';
+utf8['\\<pounds>'] = 'ยฃ';
+utf8['\\<Upsilon>'] = 'ฮฅ';
+utf8['\\<ii>'] = '๐ฆ';
+utf8['\\<hookleftarrow>'] = 'โฉ';
+utf8['\\<P>'] = '๐ซ';
+utf8['\\<threesuperior>'] = 'ยณ';
+utf8['\\<epsilon>'] = 'ฮต';
+utf8['\\<yy>'] = '๐ถ';
+utf8['\\<h>'] = '๐';
+utf8['\\<upsilon>'] = 'ฯ
';
+utf8['\\<x>'] = '๐';
+utf8['\\<not>'] = 'ยฌ';
+utf8['\\<le>'] = 'โค';
+utf8['\\<one>'] = '๐ญ';
+utf8['\\<cdots>'] = 'โฏ';
+utf8['\\<some>'] = 'ฯต';
+utf8['\\<Prod>'] = 'โ';
+utf8['\\<NN>'] = '๐';
+utf8['\\<squnion>'] = 'โ';
+utf8['\\<dd>'] = '๐ก';
+utf8['\\<top>'] = 'โค';
+utf8['\\<dieresis>'] = 'ยจ';
+utf8['\\<tt>'] = '๐ฑ';
+utf8['\\<U>'] = '๐ฐ';
+utf8['\\<unlhd>'] = 'โด';
+utf8['\\<cedilla>'] = 'ยธ';
+utf8['\\<kappa>'] = 'ฮบ';
+utf8['\\<amalg>'] = 'โจฟ';
+utf8['\\<restriction>'] = 'โพ';
+utf8['\\<struct>'] = 'โ';
+utf8['\\<m>'] = '๐';
+utf8['\\<six>'] = '๐ฒ';
+utf8['\\<midarrow>'] = 'โ';
+utf8['\\<lbrace>'] = 'โฆ';
+utf8['\\<lessapprox>'] = 'โช
';
+utf8['\\<MM>'] = '๐';
+utf8['\\<down>'] = 'โ';
+utf8['\\<oplus>'] = 'โ';
+utf8['\\<wp>'] = 'โ';
+utf8['\\<surd>'] = 'โ';
+utf8['\\<cc>'] = '๐ ';
+utf8['\\<bottom>'] = 'โฅ';
+utf8['\\<copyright>'] = 'ยฉ';
+utf8['\\<ZZ>'] = 'โจ';
+utf8['\\<union>'] = 'โช';
+utf8['\\<V>'] = '๐ฑ';
+utf8['\\<ss>'] = '๐ฐ';
+utf8['\\<unrhd>'] = 'โต';
+utf8['\\<onesuperior>'] = 'ยน';
+utf8['\\<b>'] = '๐ป';
+utf8['\\<downharpoonleft>'] = 'โ';
+utf8['\\<cdot>'] = 'โ
';
+utf8['\\<r>'] = '๐';
+utf8['\\<Midarrow>'] = 'โ';
+utf8['\\<Down>'] = 'โ';
+utf8['\\<diamondsuit>'] = 'โข';
+utf8['\\<rbrakk>'] = 'โง';
+utf8['\\<lless>'] = 'โช';
+utf8['\\<longleftrightarrow>'] = 'โท';
+utf8['\\<prec>'] = 'โบ';
+utf8['\\<emptyset>'] = 'โ
';
+utf8['\\<rparr>'] = 'โฆ';
+utf8['\\<Delta>'] = 'ฮ';
+utf8['\\<XX>'] = '๐';
+utf8['\\<parallel>'] = 'โฅ';
+utf8['\\<K>'] = '๐ฆ';
+utf8['\\<nn>'] = '๐ซ';
+utf8['\\<registered>'] = 'ยฎ';
+utf8['\\<M>'] = 'โณ';
+utf8['\\<delta>'] = 'ฮด';
+utf8['\\<threequarters>'] = 'ยพ';
+utf8['\\<g>'] = '๐';
+utf8['\\<cong>'] = 'โ
';
+utf8['\\<tau>'] = 'ฯ';
+utf8['\\<w>'] = '๐';
+utf8['\\<ge>'] = 'โฅ';
+utf8['\\<flat>'] = 'โญ';
+utf8['\\<zero>'] = '๐ฌ';
+utf8['\\<Uplus>'] = 'โจ';
+utf8['\\<longmapsto>'] = 'โผ';
+utf8['\\<supset>'] = 'โ';
+utf8['\\<in>'] = 'โ';
+utf8['\\<sqinter>'] = 'โ';
+utf8['\\<OO>'] = '๐';
+utf8['\\<updown>'] = 'โ';
+utf8['\\<circ>'] = 'โ';
+utf8['\\<rat>'] = 'โ';
+utf8['\\<stileturn>'] = 'โฃ';
+utf8['\\<ee>'] = '๐ข';
+utf8['\\<Omega>'] = 'ฮฉ';
+utf8['\\<or>'] = 'โจ';
+utf8['\\<inverse>'] = 'ยฏ';
+utf8['\\<rhd>'] = 'โณ';
+utf8['\\<uu>'] = '๐ฒ';
+utf8['\\<iota>'] = 'ฮน';
+utf8['\\<d>'] = '๐ฝ';
+utf8['\\<questiondown>'] = 'ยฟ';
+utf8['\\<Union>'] = 'โ';
+utf8['\\<omega>'] = 'ฯ';
+utf8['\\<approx>'] = 'โ';
+utf8['\\<t>'] = '๐';
+utf8['\\<Updown>'] = 'โ';
+utf8['\\<spadesuit>'] = 'โ ';
+utf8['\\<five>'] = '๐ฑ';
+utf8['\\<exists>'] = 'โ';
+utf8['\\<rceil>'] = 'โ';
+utf8['\\<JJ>'] = '๐';
+utf8['\\<minusplus>'] = 'โ';
+utf8['\\<nat>'] = 'โ';
+utf8['\\<oslash>'] = 'โ';
+utf8['\\<A>'] = '๐';
+utf8['\\<Xi>'] = 'ฮ';
+utf8['\\<currency>'] = 'ยค';
+utf8['\\<Turnstile>'] = 'โจ';
+utf8['\\<hookrightarrow>'] = 'โช';
+utf8['\\<pp>'] = '๐ญ';
+utf8['\\<Q>'] = '๐ฌ';
+utf8['\\<aleph>'] = 'โต';
+utf8['\\<acute>'] = 'ยด';
+utf8['\\<xi>'] = 'ฮพ';
+utf8['\\<simeq>'] = 'โ';
+utf8['\\<i>'] = '๐';
+utf8['\\<Join>'] = 'โ';
+utf8['\\<y>'] = '๐';
+utf8['\\<lbrakk>'] = 'โฆ';
+utf8['\\<greatersim>'] = 'โณ';
+utf8['\\<greaterapprox>'] = 'โช';
+utf8['\\<longrightarrow>'] = 'โถ';
+utf8['\\<lceil>'] = 'โ';
+utf8['\\<Gamma>'] = 'ฮ';
+utf8['\\<odot>'] = 'โ';
+utf8['\\<YY>'] = '๐';
+utf8['\\<infinity>'] = 'โ';
+utf8['\\<Sigma>'] = 'ฮฃ';
+utf8['\\<yen>'] = 'ยฅ';
+utf8['\\<int>'] = 'โค';
+utf8['\\<tturnstile>'] = 'โฉ';
+utf8['\\<oo>'] = '๐ฌ';
+utf8['\\<ointegral>'] = 'โฎ';
+utf8['\\<gamma>'] = 'ฮณ';
+utf8['\\<upharpoonleft>'] = 'โฟ';
+utf8['\\<sigma>'] = 'ฯ';
+utf8['\\<n>'] = '๐';
+utf8['\\<rbrace>'] = 'โฆ';
+utf8['\\<DD>'] = '๐';
+utf8['\\<notin>'] = 'โ';
+utf8['\\<j>'] = '๐';
+utf8['\\<uplus>'] = 'โ';
+utf8['\\<leftrightarrow>'] = 'โ';
+utf8['\\<TT>'] = '๐';
+utf8['\\<bullet>'] = 'โ';
+utf8['\\<Theta>'] = 'ฮ';
+utf8['\\<smile>'] = 'โฃ';
+utf8['\\<G>'] = '๐ข';
+utf8['\\<jj>'] = '๐ง';
+utf8['\\<inter>'] = 'โฉ';
+utf8['\\<Psi>'] = 'ฮจ';
+utf8['\\<ordfeminine>'] = 'ยช';
+utf8['\\<W>'] = '๐ฒ';
+utf8['\\<zz>'] = '๐ท';
+utf8['\\<theta>'] = 'ฮธ';
+utf8['\\<ordmasculine>'] = 'ยบ';
+utf8['\\<c>'] = '๐ผ';
+utf8['\\<psi>'] = 'ฯ';
+utf8['\\<s>'] = '๐';
+utf8['\\<Leftrightarrow>'] = 'โ';
+utf8['\\<heartsuit>'] = 'โก';
+utf8['\\<four>'] = '๐ฐ';
+
+var re_xsymbol = /\\<.*?>/g;
+
+function encodequery(ele) {
+ var text = ele.value;
+ var otext = text;
+ var pos = getCaret(ele);
+
+ xsymbols = text.match(re_xsymbol);
+ for (i in xsymbols) {
+ var repl = utf8[xsymbols[i]];
+ if (repl) {
+ text = text.replace(xsymbols[i], repl, "g");
+ }
+ }
+
+ if (text != otext) {
+ ele.value = text;
+
+ if (pos != -1) {
+ pos = pos - (otext.length - text.length);
+ setCaret(ele, pos);
+ }
+ }
+}
+
+/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */
+function getCaret(obj) {
+ var pos = -1;
+
+ if (document.selection) { // IE
+ obj.focus ();
+ var sel = document.selection.createRange();
+ var sellen = document.selection.createRange().text.length;
+ sel.moveStart ('character', -obj.value.length);
+ pos = sel.text.length - sellen;
+
+ } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko
+ pos = obj.selectionStart;
+ }
+
+ return pos;
+}
+
+/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */
+function setCaret(obj, pos) {
+ if (obj.createTextRange) {
+ var range = obj.createTextRange();
+ range.move("character", pos);
+ range.select();
+ } else if (obj.selectionStart) {
+ obj.focus();
+ obj.setSelectionRange(pos, pos);
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/www/pasting_help.html Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,19 @@
+<html>
+ <head>
+ <title>Find Theorems: help pasting from ProofGeneral</title>
+ <link rel="stylesheet" type="text/css" href="/basic.css"/>
+ </head>
+ <body>
+ <h1>Pasting theory text from Proof General</h1>
+ <ol>
+ <li>Select the text using the keyboard (<code>C-SPC</code>,
+ <code>arrow keys</code>).</li>
+ <li>Choose <code>X-Symbol</code>/<code>Other
+ Commands</code>/<code>Copy Encoded</code>.</li>
+ <li>Paste into the web browser (<code>C-v</code>).</li>
+ </ol>
+
+ <a href="/isabelle/find_theorems">Return to find_theorems</a>
+ </body>
+</html>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/xhtml.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,438 @@
+(* Title: xhtml.ML
+ Author: Timothy Bourke, NICTA
+
+Rudimentary XHTML construction.
+*)
+signature XHTML =
+sig
+ type attribute
+ type common_atts = { id : string option,
+ class : string option };
+ val noid : common_atts;
+ val id : string -> common_atts;
+ val class : string -> common_atts;
+
+ type tag
+
+ val doctype_xhtml1_0_strict: string;
+
+ val att: string -> string -> attribute
+ val bool_att: string * bool -> attribute list
+
+ val tag: string -> attribute list -> tag list -> tag
+ val tag': string -> common_atts -> tag list -> tag
+ val text: string -> tag
+ val raw_text: string -> tag
+
+ val add_attributes: attribute list -> tag -> tag
+ val append: tag -> tag list -> tag
+
+ val show: tag -> string list
+
+ val write: (string -> unit) -> tag -> unit
+ val write_open: (string -> unit) -> tag -> unit
+ val write_close: (string -> unit) -> tag -> unit
+
+ val html: { lang : string } -> tag list -> tag
+ val head: { title : string, stylesheet_href : string } -> tag list -> tag
+ val body: common_atts -> tag list -> tag
+ val divele: common_atts -> tag list -> tag
+ val span: common_atts * string -> tag
+ val span': common_atts -> tag list -> tag
+
+ val pre: common_atts -> string -> tag
+
+ val table: common_atts -> tag list -> tag
+ val thead: common_atts -> tag list -> tag
+ val tbody: common_atts -> tag list -> tag
+ val tr: tag list -> tag
+ val th: common_atts * string -> tag
+ val th': common_atts -> tag list -> tag
+ val td: common_atts * string -> tag
+ val td': common_atts -> tag list -> tag
+ val td'': common_atts * { colspan : int option, rowspan : int option }
+ -> tag list -> tag
+
+ val p: common_atts * string -> tag
+ val p': common_atts * tag list -> tag
+ val h: common_atts * int * string -> tag
+ val strong: string -> tag
+ val em: string -> tag
+ val a: { href : string, text : string } -> tag
+
+ val ul: common_atts * tag list -> tag
+ val ol: common_atts * tag list -> tag
+ val dl: common_atts * (string * tag) list -> tag
+
+ val alternate_class: { class0 : string, class1 : string }
+ -> tag list -> tag list
+
+ val form: common_atts * { method : string, action : string }
+ -> tag list -> tag
+
+ datatype input_type =
+ TextInput of { value: string option, maxlength: int option }
+ | Password of int option
+ | Checkbox of { checked : bool, value : string option }
+ | Radio of { checked : bool, value : string option }
+ | Submit
+ | Reset
+ | Hidden
+ | Image of { src : string, alt : string }
+ | File of { accept : string }
+ | Button;
+
+ val input: common_atts * { name : string, itype : input_type } -> tag
+ val select: common_atts * { name : string, value : string option }
+ -> string list -> tag
+ val label: common_atts * { for: string } * string -> tag
+
+ val reset_button: common_atts -> tag
+ val submit_button: common_atts -> tag
+
+ datatype event =
+ (* global *)
+ OnClick
+ | OnDblClick
+ | OnMouseDown
+ | OnMouseUp
+ | OnMouseOver
+ | OnMouseMove
+ | OnMouseOut
+ | OnKeyPress
+ | OnKeyDown
+ | OnKeyUp
+ (* anchor/label/input/select/textarea/button/area *)
+ | OnFocus
+ | OnBlur
+ (* form *)
+ | OnSubmit
+ | OnReset
+ (* input/textarea *)
+ | OnSelect
+ (* input/select/textarea *)
+ | OnChange
+ (* body *)
+ | OnLoad
+ | OnUnload;
+
+ val script: common_atts * { script_type: string, src: string } -> tag
+ val add_script: event * string -> tag -> tag
+end;
+
+structure Xhtml : XHTML =
+struct
+
+type attribute = string * string;
+type common_atts = {
+ id : string option,
+ class : string option
+ };
+val noid = { id = NONE, class = NONE };
+fun id s = { id = SOME s, class = NONE };
+fun class s = { id = NONE, class = SOME s };
+
+fun from_common { id = NONE, class = NONE } = []
+ | from_common { id = SOME i, class = NONE } = [("id", i)]
+ | from_common { id = NONE, class = SOME c } = [("class", c)]
+ | from_common { id = SOME i, class = SOME c } = [("id", i), ("class", c)];
+
+val update_atts =
+ AList.join (op = : string * string -> bool) (fn _ => snd);
+
+datatype tag = Tag of (string * attribute list * tag list)
+ | Text of string
+ | RawText of string;
+
+fun is_text (Tag _) = false
+ | is_text (Text _) = true
+ | is_text (RawText _) = true;
+
+fun is_tag (Tag _) = true
+ | is_tag (Text _) = false
+ | is_tag (RawText _) = false;
+
+val att = pair;
+
+fun bool_att (nm, true) = [(nm, nm)]
+ | bool_att (nm, false) = [];
+
+fun tag name atts inner = Tag (name, atts, inner);
+fun tag' name common_atts inner = Tag (name, from_common common_atts, inner);
+fun text t = Text t;
+fun raw_text t = RawText t;
+
+fun add_attributes atts' (Tag (nm, atts, inner)) =
+ Tag (nm, update_atts (atts, atts'), inner)
+ | add_attributes _ t = t;
+
+fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
+ | append _ _ = raise Fail "cannot append to a text element";
+
+fun show_att (n, v) = concat [" ", n, "=\"", XML.text v, "\""];
+
+fun show_text (Text t) = XML.text t
+ | show_text (RawText t) = t
+ | show_text _ = raise Fail "Bad call to show_text.";
+
+fun show (Text t) = [XML.text t]
+ | show (RawText t) = [t]
+ | show (Tag (nm, atts, inner)) =
+ (["<", nm] @ map show_att atts
+ @
+ (if length inner = 0
+ then ["/>"]
+ else List.concat (
+ [[">"]]
+ @
+ map show inner
+ @
+ [["</", nm, ">"]]
+ )));
+
+fun write pr =
+ let
+ fun f (Text t) = (pr o XML.text) t
+ | f (RawText t) = pr t
+ | f (Tag (nm, atts, inner)) = (
+ pr "<";
+ pr nm;
+ app (pr o show_att) atts;
+ if length inner = 0
+ then pr "/>"
+ else (
+ pr ">";
+ app f inner;
+ pr ("</" ^ nm ^ ">")
+ ))
+ in f end;
+
+(* Print all opening tags down into the tree until a branch of degree > 1 is
+ found, in which case print everything before the last tag, which is then
+ opened. *)
+fun write_open pr =
+ let
+ fun f (Text t) = (pr o XML.text) t
+ | f (RawText t) = pr t
+ | f (Tag (nm, atts, [])) =
+ (pr "<"; pr nm; app (pr o show_att) atts; pr ">")
+ | f (Tag (nm, atts, xs)) =
+ (pr "<"; pr nm; app (pr o show_att) atts; pr ">";
+ (case take_suffix is_text xs of
+ ([], _) => ()
+ | (b, _) =>
+ let val (xs, x) = split_last b;
+ in app (write pr) xs; f x end));
+ in f end;
+
+(* Print matching closing tags for write_open. *)
+fun write_close pr =
+ let
+ fun close nm = pr ("</" ^ nm ^ ">");
+ val pr_text = app (pr o show_text);
+
+ fun f (Text t) = ()
+ | f (RawText t) = ()
+ | f (Tag (nm, _, [])) = close nm
+ | f (Tag (nm, _, xs)) =
+ (case take_suffix is_text xs of
+ ([], text) => pr_text text
+ | (b, text) =>
+ let val (xs, x) = split_last b;
+ in f x; close nm; pr_text text end);
+ in f end;
+
+fun html { lang } tags = Tag ("html",
+ [("xmlns", "http://www.w3.org/1999/xhtml"),
+ ("xml:lang", lang)],
+ tags);
+
+fun head { title, stylesheet_href } inner = let
+ val link =
+ Tag ("link",
+ [("rel", "stylesheet"),
+ ("type", "text/css"),
+ ("href", stylesheet_href)], []);
+ val title = Tag ("title", [], [Text title]);
+ val charset = Tag ("meta",
+ [("http-equiv", "Content-type"),
+ ("content", "text/html; charset=UTF-8")], []);
+ in Tag ("head", [], link::title::charset::inner) end;
+
+fun body common_atts tags = Tag ("body", from_common common_atts, tags);
+
+fun divele common_atts tags = Tag ("div", from_common common_atts, tags);
+fun span (common_atts, t) = Tag ("span", from_common common_atts, [Text t]);
+fun span' common_atts tags = Tag ("span", from_common common_atts, tags);
+
+fun pre common_atts rt = Tag ("pre", from_common common_atts, [RawText rt]);
+
+fun ostr_att (nm, NONE) = []
+ | ostr_att (nm, SOME s) = [(nm, s)];
+val oint_att = ostr_att o apsnd (Option.map Int.toString);
+
+val table = tag' "table";
+val thead = tag' "thead";
+val tbody = tag' "tbody";
+val tr = tag "tr" [];
+fun th (common_atts, t) = Tag ("th", from_common common_atts, [Text t]);
+fun th' common_atts tags = Tag ("th", from_common common_atts, tags);
+fun td (common_atts, t) = Tag ("td", from_common common_atts, [Text t]);
+fun td' common_atts tags = Tag ("td", from_common common_atts, tags);
+fun td'' (common_atts, { colspan, rowspan }) tags =
+ Tag ("td",
+ from_common common_atts
+ @ oint_att ("colspan", colspan)
+ @ oint_att ("rowspan", rowspan),
+ tags);
+
+fun p (common_atts, t) = Tag ("p", from_common common_atts, [Text t]);
+fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags);
+
+fun h (common_atts, i, text) =
+ Tag ("h" ^ Int.toString i, from_common common_atts, [Text text]);
+
+fun strong t = Tag ("strong", [], [Text t]);
+fun em t = Tag ("em", [], [Text t]);
+fun a { href, text } = Tag ("a", [("href", href)], [Text text]);
+
+fun to_li tag = Tag ("li", [], [tag]);
+fun ul (common_atts, lis) = Tag ("ul", from_common common_atts, map to_li lis);
+fun ol (common_atts, lis) = Tag ("ol", from_common common_atts, map to_li lis);
+
+fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
+ Tag ("dd", [], [tag])];
+fun dl (common_atts, dtdds) =
+ Tag ("dl", from_common common_atts, (List.concat o map to_dtdd) dtdds);
+
+fun alternate_class { class0, class1 } rows = let
+ fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)
+ | f ((false, xs), x) = (true, add_attributes [("class", class1)] x :: xs);
+ in Library.foldl f ((true, []), rows) |> snd |> rev end;
+
+fun form (common_atts as { id, ... }, { method, action }) tags =
+ Tag ("form",
+ [("method", method),
+ ("action", action)]
+ @ from_common common_atts, tags);
+
+datatype input_type =
+ TextInput of { value: string option, maxlength: int option }
+ | Password of int option
+ | Checkbox of { checked : bool, value : string option }
+ | Radio of { checked : bool, value : string option }
+ | Submit
+ | Reset
+ | Hidden
+ | Image of { src : string, alt : string }
+ | File of { accept : string }
+ | Button;
+
+fun from_checked { checked = false, value = NONE } = []
+ | from_checked { checked = true, value = NONE } = [("checked", "checked")]
+ | from_checked { checked = false, value = SOME v } = [("value", v)]
+ | from_checked { checked = true, value = SOME v } =
+ [("checked", "checked"), ("value", v)];
+
+fun input_atts (TextInput { value, maxlength }) =
+ ("type", "text")
+ :: ostr_att ("value", value)
+ @ oint_att ("maxlength", maxlength)
+ | input_atts (Password NONE) = [("type", "password")]
+ | input_atts (Password (SOME i)) =
+ [("type", "password"), ("maxlength", Int.toString i)]
+ | input_atts (Checkbox checked) =
+ ("type", "checkbox") :: from_checked checked
+ | input_atts (Radio checked) = ("type", "radio") :: from_checked checked
+ | input_atts Submit = [("type", "submit")]
+ | input_atts Reset = [("type", "reset")]
+ | input_atts Hidden = [("type", "hidden")]
+ | input_atts (Image { src, alt }) =
+ [("type", "image"), ("src", src), ("alt", alt)]
+ | input_atts (File { accept }) = [("type", "file"), ("accept", accept)]
+ | input_atts Button = [("type", "button")];
+
+fun input (common_atts, { name, itype }) =
+ Tag ("input",
+ input_atts itype @ [("name", name)] @ from_common common_atts,
+ []);
+
+fun reset_button common_atts =
+ Tag ("input", input_atts Reset @ from_common common_atts, []);
+
+fun submit_button common_atts =
+ Tag ("input", input_atts Submit @ from_common common_atts, []);
+
+
+fun select (common_atts, { name, value }) options =
+ let
+ fun is_selected t =
+ (case value of
+ NONE => []
+ | SOME s => if t = s then bool_att ("selected", true) else []);
+ fun to_option t = Tag ("option", is_selected t, [Text t]);
+ in
+ Tag ("select",
+ ("name", name) :: from_common common_atts,
+ map to_option options)
+ end;
+
+fun label (common_atts, { for }, text) =
+ Tag ("label", ("for", for) :: from_common common_atts, [Text text]);
+
+datatype event =
+ OnClick
+ | OnDblClick
+ | OnMouseDown
+ | OnMouseUp
+ | OnMouseOver
+ | OnMouseMove
+ | OnMouseOut
+ | OnKeyPress
+ | OnKeyDown
+ | OnKeyUp
+ | OnFocus
+ | OnBlur
+ | OnSubmit
+ | OnReset
+ | OnSelect
+ | OnChange
+ | OnLoad
+ | OnUnload;
+
+fun event_to_str OnClick = "onclick"
+ | event_to_str OnDblClick = "ondblclick"
+ | event_to_str OnMouseDown = "onmousedown"
+ | event_to_str OnMouseUp = "onmouseup"
+ | event_to_str OnMouseOver = "onmouseover"
+ | event_to_str OnMouseMove = "onmousemove"
+ | event_to_str OnMouseOut = "onmouseout"
+ | event_to_str OnKeyPress = "onkeypress"
+ | event_to_str OnKeyDown = "onkeydown"
+ | event_to_str OnKeyUp = "onkeyup"
+ | event_to_str OnFocus = "onfocus"
+ | event_to_str OnBlur = "onblur"
+ | event_to_str OnSubmit = "onsubmit"
+ | event_to_str OnReset = "onreset"
+ | event_to_str OnSelect = "onselect"
+ | event_to_str OnChange = "onchange"
+ | event_to_str OnLoad = "onload"
+ | event_to_str OnUnload = "onunload";
+
+fun script (common_atts, {script_type, src}) =
+ Tag ("script",
+ ("type", script_type)
+ :: ("src", src)
+ :: from_common common_atts, [text ""]);
+
+fun add_script (evty, script) (Tag (name, atts, inner))
+ = Tag (name, AList.update (op =) (event_to_str evty, script) atts, inner)
+ | add_script _ t = t;
+
+
+val doctype_xhtml1_0_strict =
+ "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
+ \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
+
+end;
+