# HG changeset patch # User kleing # Date 1258702604 -39600 # Node ID f6a4da31f2f1293cca2cb86ef44b8ef64249802e # Parent e08c9f755fca644fc790dbf2d298bd5f4df8b8ff WWW_Find component: find_theorems via web browser diff -r e08c9f755fca -r f6a4da31f2f1 etc/components --- 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 diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/IsaMakefile --- /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) diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/ROOT.ML --- /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 () diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/doc/README --- /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 + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/doc/design.tex --- /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+\+. +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} diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/echo.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/etc/settings --- /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" diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/find_theorems.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/html_unicode.ML --- /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 + [("\", 2), + ("\", 2), + ("\", 2), + ("\", 2), + ("\", 2), + ("\", 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 "" "") (output_sym s); + fun output_sup s = apsnd (enclose "" "") (output_sym s); + fun output_loc s = apsnd (enclose "" "") (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 = ("", ""); + +val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name); + +end; diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/http_status.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/http_util.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/lib/Tools/wwwfind --- /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 + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/lighttpd.conf --- /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" + ))) + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/mime.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/scgi_req.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/scgi_server.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/socket_util.ML --- /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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/unicode_symbols.ML --- /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 = "\"; + + 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; + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/www/basic.css --- /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; +} + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/www/find_theorems.js --- /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['\\'] = 'โŠ‡'; +utf8['\\'] = '๐”Ž'; +utf8['\\'] = 'โ†‘'; +utf8['\\'] = 'โŠ—'; +utf8['\\'] = '๐”ž'; +utf8['\\'] = 'โ€ '; +utf8['\\'] = 'โŒข'; +utf8['\\'] = 'ยซ'; +utf8['\\'] = '๐”ฎ'; +utf8['\\'] = '๐’ณ'; +utf8['\\'] = 'โ–น'; +utf8['\\'] = 'ยป'; +utf8['\\'] = 'ฮฝ'; +utf8['\\'] = 'โˆผ'; +utf8['\\'] = 'โ‡'; +utf8['\\

'] = '๐—‰'; +utf8['\\'] = 'โ‡‘'; +utf8['\\'] = 'โ‰œ'; +utf8['\\'] = '๐Ÿต'; +utf8['\\'] = 'โ‰ผ'; +utf8['\\'] = 'โˆ‡'; +utf8['\\'] = '๐”‰'; +utf8['\\'] = 'โ„‘'; +utf8['\\'] = '๐”™'; +utf8['\\'] = 'โฃ'; +utf8['\\'] = 'โˆง'; +utf8['\\'] = 'โ†ฆ'; +utf8['\\'] = '๐”ฉ'; +utf8['\\'] = 'โ„ฑ'; +utf8['\\'] = 'ยฐ'; +utf8['\\'] = 'ฮฒ'; +utf8['\\'] = 'โˆท'; +utf8['\\'] = '๐”น'; +utf8['\\'] = '๐–พ'; +utf8['\\'] = 'โ—Š'; +utf8['\\'] = '๐—Ž'; +utf8['\\'] = 'โ™ฏ'; +utf8['\\'] = 'โŸบ'; +utf8['\\'] = 'โจ‚'; +utf8['\\'] = '๐”ˆ'; +utf8['\\'] = 'โ„'; +utf8['\\'] = '๐”˜'; +utf8['\\'] = 'ยก'; +utf8['\\'] = 'โ€ฆ'; +utf8['\\'] = '๐’ฉ'; +utf8['\\'] = '๐”จ'; +utf8['\\'] = 'ยฑ'; +utf8['\\'] = 'โ„ฐ'; +utf8['\\'] = 'โ–ณ'; +utf8['\\'] = 'ฮท'; +utf8['\\'] = 'โ—ƒ'; +utf8['\\'] = 'ฯ‡'; +utf8['\\'] = '๐—“'; +utf8['\\'] = 'ห'; +utf8['\\'] = 'โˆ‚'; +utf8['\\'] = '๐Ÿฏ'; +utf8['\\'] = 'โ‰ฒ'; +utf8['\\'] = 'โŠ‚'; +utf8['\\'] = 'โ„‹'; +utf8['\\'] = 'โ†'; +utf8['\\'] = '๐”“'; +utf8['\\'] = 'โŠ’'; +utf8['\\'] = 'โ„›'; +utf8['\\'] = 'โจ'; +utf8['\\'] = '๐’ž'; +utf8['\\'] = 'โ€ก'; +utf8['\\'] = '๐”ฃ'; +utf8['\\'] = 'โŠข'; +utf8['\\'] = 'ยฆ'; +utf8['\\'] = 'โˆ'; +utf8['\\'] = '๐’ฎ'; +utf8['\\'] = '๐”ณ'; +utf8['\\'] = 'โŠฒ'; +utf8['\\'] = 'ยถ'; +utf8['\\'] = 'ฮผ'; +utf8['\\'] = 'โ‡€'; +utf8['\\'] = 'โ‹‚'; +utf8['\\'] = '๐—ˆ'; +utf8['\\'] = 'โ‰'; +utf8['\\'] = 'โ‡'; +utf8['\\'] = 'โจ…'; +utf8['\\'] = '๐Ÿด'; +utf8['\\'] = 'โ‰ฝ'; +utf8['\\'] = 'โˆ€'; +utf8['\\'] = 'โ„‚'; +utf8['\\'] = '๐”Š'; +utf8['\\'] = 'โˆ'; +utf8['\\'] = 'โ„’'; +utf8['\\'] = '๐”š'; +utf8['\\'] = 'โ†'; +utf8['\\'] = '๐’Ÿ'; +utf8['\\'] = 'โˆ '; +utf8['\\

'] = 'ยง'; +utf8['\\'] = 'โŠซ'; +utf8['\\'] = '๐”ช'; +utf8['\\'] = '๐’ฏ'; +utf8['\\'] = 'ฮฑ'; +utf8['\\'] = 'โ†ฝ'; +utf8['\\'] = 'ฯ'; +utf8['\\'] = 'โ‰€'; +utf8['\\'] = '๐—…'; +utf8['\\'] = 'โ‰'; +utf8['\\'] = 'ร—'; +utf8['\\'] = 'โ‰ '; +utf8['\\'] = 'โŸฉ'; +utf8['\\
'] = 'รท'; +utf8['\\'] = 'โŸน'; +utf8['\\'] = '๐”…'; +utf8['\\'] = 'โŠ'; +utf8['\\'] = 'โ†’'; +utf8['\\'] = 'โ„'; +utf8['\\'] = '๐”ฅ'; +utf8['\\'] = 'ฮฆ'; +utf8['\\'] = 'โˆซ'; +utf8['\\'] = 'โ„ญ'; +utf8['\\'] = 'โ‚ฌ'; +utf8['\\'] = '๐”ต'; +utf8['\\'] = '๐’ด'; +utf8['\\'] = 'ฮถ'; +utf8['\\'] = 'โŸต'; +utf8['\\'] = '๐–บ'; +utf8['\\'] = 'ยผ'; +utf8['\\'] = 'โ‹€'; +utf8['\\'] = 'โ‡‚'; +utf8['\\'] = 'ฯ†'; +utf8['\\'] = '๐—Š'; +utf8['\\'] = 'โ‡’'; +utf8['\\'] = 'โ™ฃ'; +utf8['\\'] = 'โ‰ซ'; +utf8['\\'] = '๐Ÿฎ'; +utf8['\\'] = 'โ‰ป'; +utf8['\\'] = '๐”„'; +utf8['\\'] = 'โฆ‡'; +utf8['\\'] = 'โจ†'; +utf8['\\'] = 'โ„Œ'; +utf8['\\'] = 'โŠ‘'; +utf8['\\'] = '๐””'; +utf8['\\'] = 'โˆ–'; +utf8['\\'] = 'ฮ›'; +utf8['\\'] = 'โ„œ'; +utf8['\\'] = '๐’ฅ'; +utf8['\\'] = '๐”ค'; +utf8['\\'] = 'ยญ'; +utf8['\\'] = 'โ„ฌ'; +utf8['\\'] = '๐’ต'; +utf8['\\'] = '๐”ด'; +utf8['\\'] = 'ฮป'; +utf8['\\'] = 'ยฝ'; +utf8['\\'] = '๐–ฟ'; +utf8['\\'] = 'โ‹'; +utf8['\\'] = '๐—'; +utf8['\\'] = 'โ™ฎ'; +utf8['\\'] = '๐Ÿณ'; +utf8['\\'] = 'โจ'; +utf8['\\'] = 'โŠ†'; +utf8['\\'] = 'โŒ‹'; +utf8['\\'] = '๐”'; +utf8['\\'] = 'โˆ‘'; +utf8['\\'] = 'โŠ–'; +utf8['\\'] = '๐”Ÿ'; +utf8['\\'] = 'ฮ '; +utf8['\\'] = 'ยข'; +utf8['\\'] = 'โ—‡'; +utf8['\\'] = 'โ„ง'; +utf8['\\'] = '๐’ช'; +utf8['\\'] = '๐”ฏ'; +utf8['\\'] = 'ยฒ'; +utf8['\\'] = 'โ†ผ'; +utf8['\\'] = 'ฯ€'; +utf8['\\'] = '๐—„'; +utf8['\\'] = 'โ‹†'; +utf8['\\'] = 'โ‡Œ'; +utf8['\\'] = 'โ‰ก'; +utf8['\\'] = 'โŸจ'; +utf8['\\'] = 'โŸธ'; +utf8['\\'] = 'โˆ„'; +utf8['\\'] = 'โจ€'; +utf8['\\'] = 'โŒŠ'; +utf8['\\'] = 'โŠ'; +utf8['\\'] = '๐”–'; +utf8['\\'] = 'โ–ก'; +utf8['\\'] = 'ฤฑ'; +utf8['\\'] = 'ยฃ'; +utf8['\\'] = 'ฮฅ'; +utf8['\\'] = '๐”ฆ'; +utf8['\\'] = 'โ†ฉ'; +utf8['\\

'] = '๐’ซ'; +utf8['\\'] = 'ยณ'; +utf8['\\'] = 'ฮต'; +utf8['\\'] = '๐”ถ'; +utf8['\\'] = '๐—'; +utf8['\\'] = 'ฯ…'; +utf8['\\'] = '๐—‘'; +utf8['\\'] = 'ยฌ'; +utf8['\\'] = 'โ‰ค'; +utf8['\\'] = '๐Ÿญ'; +utf8['\\'] = 'โ‹ฏ'; +utf8['\\'] = 'ฯต'; +utf8['\\'] = 'โˆ'; +utf8['\\'] = '๐”‘'; +utf8['\\'] = 'โŠ”'; +utf8['\\

'] = '๐”‡'; +utf8['\\'] = 'โˆ‰'; +utf8['\\'] = '๐—ƒ'; +utf8['\\'] = 'โŠŽ'; +utf8['\\'] = 'โ†”'; +utf8['\\'] = '๐”—'; +utf8['\\'] = 'โˆ™'; +utf8['\\'] = 'ฮ˜'; +utf8['\\'] = 'โŒฃ'; +utf8['\\'] = '๐’ข'; +utf8['\\'] = '๐”ง'; +utf8['\\'] = 'โˆฉ'; +utf8['\\'] = 'ฮจ'; +utf8['\\'] = 'ยช'; +utf8['\\'] = '๐’ฒ'; +utf8['\\'] = '๐”ท'; +utf8['\\'] = 'ฮธ'; +utf8['\\'] = 'ยบ'; +utf8['\\'] = '๐–ผ'; +utf8['\\'] = 'ฯˆ'; +utf8['\\'] = '๐—Œ'; +utf8['\\'] = 'โ‡”'; +utf8['\\'] = 'โ™ก'; +utf8['\\'] = '๐Ÿฐ'; + +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); + } +} + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/www/pasting_help.html --- /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 @@ + + + Find Theorems: help pasting from ProofGeneral + + + +

Pasting theory text from Proof General

+
    +
  1. Select the text using the keyboard (C-SPC, + arrow keys).
    2. +
  2. Choose X-Symbol/Other + Commands/Copy Encoded.
    3. +
  3. Paste into the web browser (C-v).
    4. +
+ + Return to find_theorems + + + diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/xhtml.ML --- /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 + @ + [[""]] + ))); + +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 ("") + )) + 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 (""); + 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 = + "\n"; + +end; +
'] = '๐”ก'; +utf8['\\'] = 'โŠค'; +utf8['\\'] = 'ยจ'; +utf8['\\'] = '๐”ฑ'; +utf8['\\'] = '๐’ฐ'; +utf8['\\'] = 'โŠด'; +utf8['\\'] = 'ยธ'; +utf8['\\'] = 'ฮบ'; +utf8['\\'] = 'โจฟ'; +utf8['\\'] = 'โ†พ'; +utf8['\\'] = 'โ‹„'; +utf8['\\'] = '๐—†'; +utf8['\\'] = '๐Ÿฒ'; +utf8['\\'] = 'โ”€'; +utf8['\\'] = 'โฆƒ'; +utf8['\\'] = 'โช…'; +utf8['\\'] = '๐”'; +utf8['\\'] = 'โ†“'; +utf8['\\'] = 'โŠ•'; +utf8['\\'] = 'โ„˜'; +utf8['\\'] = 'โˆš'; +utf8['\\'] = '๐” '; +utf8['\\'] = 'โŠฅ'; +utf8['\\'] = 'ยฉ'; +utf8['\\'] = 'โ„จ'; +utf8['\\'] = 'โˆช'; +utf8['\\'] = '๐’ฑ'; +utf8['\\'] = '๐”ฐ'; +utf8['\\'] = 'โŠต'; +utf8['\\'] = 'ยน'; +utf8['\\'] = '๐–ป'; +utf8['\\'] = 'โ‡ƒ'; +utf8['\\'] = 'โ‹…'; +utf8['\\'] = '๐—‹'; +utf8['\\'] = 'โ•'; +utf8['\\'] = 'โ‡“'; +utf8['\\'] = 'โ™ข'; +utf8['\\'] = 'โŸง'; +utf8['\\'] = 'โ‰ช'; +utf8['\\'] = 'โŸท'; +utf8['\\'] = 'โ‰บ'; +utf8['\\'] = 'โˆ…'; +utf8['\\'] = 'โฆˆ'; +utf8['\\'] = 'ฮ”'; +utf8['\\'] = '๐”›'; +utf8['\\'] = 'โˆฅ'; +utf8['\\'] = '๐’ฆ'; +utf8['\\'] = '๐”ซ'; +utf8['\\'] = 'ยฎ'; +utf8['\\'] = 'โ„ณ'; +utf8['\\'] = 'ฮด'; +utf8['\\'] = 'ยพ'; +utf8['\\'] = '๐—€'; +utf8['\\'] = 'โ‰…'; +utf8['\\'] = 'ฯ„'; +utf8['\\'] = '๐—'; +utf8['\\'] = 'โ‰ฅ'; +utf8['\\'] = 'โ™ญ'; +utf8['\\'] = '๐Ÿฌ'; +utf8['\\'] = 'โจ„'; +utf8['\\'] = 'โŸผ'; +utf8['\\'] = 'โŠƒ'; +utf8['\\'] = 'โˆˆ'; +utf8['\\'] = 'โŠ“'; +utf8['\\'] = '๐”’'; +utf8['\\'] = 'โ†•'; +utf8['\\'] = 'โˆ˜'; +utf8['\\'] = 'โ„š'; +utf8['\\'] = 'โŠฃ'; +utf8['\\'] = '๐”ข'; +utf8['\\'] = 'ฮฉ'; +utf8['\\'] = 'โˆจ'; +utf8['\\'] = 'ยฏ'; +utf8['\\'] = 'โŠณ'; +utf8['\\'] = '๐”ฒ'; +utf8['\\'] = 'ฮน'; +utf8['\\'] = '๐–ฝ'; +utf8['\\'] = 'ยฟ'; +utf8['\\'] = 'โ‹ƒ'; +utf8['\\'] = 'ฯ‰'; +utf8['\\'] = 'โ‰ˆ'; +utf8['\\'] = '๐—'; +utf8['\\'] = 'โ‡•'; +utf8['\\'] = 'โ™ '; +utf8['\\'] = '๐Ÿฑ'; +utf8['\\'] = 'โˆƒ'; +utf8['\\'] = 'โŒ‰'; +utf8['\\'] = '๐”'; +utf8['\\'] = 'โˆ“'; +utf8['\\'] = 'โ„•'; +utf8['\\'] = 'โŠ˜'; +utf8['\\'] = '๐’œ'; +utf8['\\'] = 'ฮž'; +utf8['\\'] = 'ยค'; +utf8['\\'] = 'โŠจ'; +utf8['\\'] = 'โ†ช'; +utf8['\\'] = '๐”ญ'; +utf8['\\'] = '๐’ฌ'; +utf8['\\'] = 'โ„ต'; +utf8['\\'] = 'ยด'; +utf8['\\'] = 'ฮพ'; +utf8['\\'] = 'โ‰ƒ'; +utf8['\\'] = '๐—‚'; +utf8['\\'] = 'โ‹ˆ'; +utf8['\\'] = '๐—’'; +utf8['\\'] = 'โŸฆ'; +utf8['\\'] = 'โ‰ณ'; +utf8['\\'] = 'โช†'; +utf8['\\'] = 'โŸถ'; +utf8['\\'] = 'โŒˆ'; +utf8['\\'] = 'ฮ“'; +utf8['\\'] = 'โŠ™'; +utf8['\\'] = '๐”œ'; +utf8['\\'] = 'โˆž'; +utf8['\\'] = 'ฮฃ'; +utf8['\\'] = 'ยฅ'; +utf8['\\'] = 'โ„ค'; +utf8['\\'] = 'โŠฉ'; +utf8['\\'] = '๐”ฌ'; +utf8['\\'] = 'โˆฎ'; +utf8['\\'] = 'ฮณ'; +utf8['\\'] = 'โ†ฟ'; +utf8['\\'] = 'ฯƒ'; +utf8['\\'] = '๐—‡'; +utf8['\\'] = 'โฆ„'; +utf8['\\