--- a/NEWS Sat Apr 26 06:43:06 2014 +0200
+++ b/NEWS Sat Apr 26 21:37:09 2014 +1000
@@ -691,7 +691,8 @@
incompatibility for old tools that do not use the $ISABELLE_PROCESS
settings variable yet.
-
+* Retired the now unused Isabelle tool "wwwfind". Similar functionality
+may be integrated into PIDE/jEdit at a later point.
New in Isabelle2013-2 (December 2013)
-------------------------------------
--- a/etc/components Sat Apr 26 06:43:06 2014 +0200
+++ b/etc/components Sat Apr 26 21:37:09 2014 +1000
@@ -1,7 +1,6 @@
src/Tools/Code
src/Tools/jEdit
src/Tools/Graphview
-src/Tools/WWW_Find
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
--- a/src/Tools/ROOT Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Tools/ROOT Sat Apr 26 21:37:09 2014 +1000
@@ -1,6 +1,3 @@
-session WWW_Find in WWW_Find = Pure +
- theories [condition = ISABELLE_POLYML] WWW_Find
-
session Spec_Check in Spec_Check = Pure +
theories
Spec_Check
--- a/src/Tools/WWW_Find/Start_WWW_Find.thy Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Load this theory to start the WWW_Find server on port defined by environment
- variable "SCGIPORT". Used by the isabelle wwwfind tool.
-*)
-
-theory Start_WWW_Find imports WWW_Find begin
-
-ML {*
- val port = Markup.parse_int (getenv "SCGIPORT");
- ScgiServer.server' 10 "/" port;
-*}
-
-end
-
--- a/src/Tools/WWW_Find/WWW_Find.thy Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-theory WWW_Find
-imports Pure
-begin
-
-ML_file "unicode_symbols.ML"
-ML_file "html_unicode.ML"
-ML_file "mime.ML"
-ML_file "http_status.ML"
-ML_file "http_util.ML"
-ML_file "xhtml.ML"
-ML_file "socket_util.ML"
-ML_file "scgi_req.ML"
-ML_file "scgi_server.ML"
-ML_file "echo.ML"
-ML_file "html_templates.ML"
-ML_file "find_theorems.ML"
-
-end
-
--- a/src/Tools/WWW_Find/doc/README Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-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
-
--- a/src/Tools/WWW_Find/doc/design.tex Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,326 +0,0 @@
-% 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 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}
--- a/src/Tools/WWW_Find/echo.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Tools/WWW_Find/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;
-
--- a/src/Tools/WWW_Find/etc/settings Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-LIGHTTPD="/usr/sbin/lighttpd"
-
-WWWFINDDIR="$COMPONENT"
-WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"
--- a/src/Tools/WWW_Find/etc/symbols Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,357 +0,0 @@
-# Default interpretation of some Isabelle symbols (outdated version for WWW_Find)
-
-\<zero> code: 0x01d7ec group: digit
-\<one> code: 0x01d7ed group: digit
-\<two> code: 0x01d7ee group: digit
-\<three> code: 0x01d7ef group: digit
-\<four> code: 0x01d7f0 group: digit
-\<five> code: 0x01d7f1 group: digit
-\<six> code: 0x01d7f2 group: digit
-\<seven> code: 0x01d7f3 group: digit
-\<eight> code: 0x01d7f4 group: digit
-\<nine> code: 0x01d7f5 group: digit
-\<A> code: 0x01d49c group: letter
-\<B> code: 0x00212c group: letter
-\<C> code: 0x01d49e group: letter
-\<D> code: 0x01d49f group: letter
-\<E> code: 0x002130 group: letter
-\<F> code: 0x002131 group: letter
-\<G> code: 0x01d4a2 group: letter
-\<H> code: 0x00210b group: letter
-\<I> code: 0x002110 group: letter
-\<J> code: 0x01d4a5 group: letter
-\<K> code: 0x01d4a6 group: letter
-\<L> code: 0x002112 group: letter
-\<M> code: 0x002133 group: letter
-\<N> code: 0x01d4a9 group: letter
-\<O> code: 0x01d4aa group: letter
-\<P> code: 0x01d4ab group: letter
-\<Q> code: 0x01d4ac group: letter
-\<R> code: 0x00211b group: letter
-\<S> code: 0x01d4ae group: letter
-\<T> code: 0x01d4af group: letter
-\<U> code: 0x01d4b0 group: letter
-\<V> code: 0x01d4b1 group: letter
-\<W> code: 0x01d4b2 group: letter
-\<X> code: 0x01d4b3 group: letter
-\<Y> code: 0x01d4b4 group: letter
-\<Z> code: 0x01d4b5 group: letter
-\<a> code: 0x01d5ba group: letter
-\<b> code: 0x01d5bb group: letter
-\<c> code: 0x01d5bc group: letter
-\<d> code: 0x01d5bd group: letter
-\<e> code: 0x01d5be group: letter
-\<f> code: 0x01d5bf group: letter
-\<g> code: 0x01d5c0 group: letter
-\<h> code: 0x01d5c1 group: letter
-\<i> code: 0x01d5c2 group: letter
-\<j> code: 0x01d5c3 group: letter
-\<k> code: 0x01d5c4 group: letter
-\<l> code: 0x01d5c5 group: letter
-\<m> code: 0x01d5c6 group: letter
-\<n> code: 0x01d5c7 group: letter
-\<o> code: 0x01d5c8 group: letter
-\<p> code: 0x01d5c9 group: letter
-\<q> code: 0x01d5ca group: letter
-\<r> code: 0x01d5cb group: letter
-\<s> code: 0x01d5cc group: letter
-\<t> code: 0x01d5cd group: letter
-\<u> code: 0x01d5ce group: letter
-\<v> code: 0x01d5cf group: letter
-\<w> code: 0x01d5d0 group: letter
-\<x> code: 0x01d5d1 group: letter
-\<y> code: 0x01d5d2 group: letter
-\<z> code: 0x01d5d3 group: letter
-\<AA> code: 0x01d504 group: letter
-\<BB> code: 0x01d505 group: letter
-\<CC> code: 0x00212d group: letter
-\<DD> code: 0x01d507 group: letter
-\<EE> code: 0x01d508 group: letter
-\<FF> code: 0x01d509 group: letter
-\<GG> code: 0x01d50a group: letter
-\<HH> code: 0x00210c group: letter
-\<II> code: 0x002111 group: letter
-\<JJ> code: 0x01d50d group: letter
-\<KK> code: 0x01d50e group: letter
-\<LL> code: 0x01d50f group: letter
-\<MM> code: 0x01d510 group: letter
-\<NN> code: 0x01d511 group: letter
-\<OO> code: 0x01d512 group: letter
-\<PP> code: 0x01d513 group: letter
-\<QQ> code: 0x01d514 group: letter
-\<RR> code: 0x00211c group: letter
-\<SS> code: 0x01d516 group: letter
-\<TT> code: 0x01d517 group: letter
-\<UU> code: 0x01d518 group: letter
-\<VV> code: 0x01d519 group: letter
-\<WW> code: 0x01d51a group: letter
-\<XX> code: 0x01d51b group: letter
-\<YY> code: 0x01d51c group: letter
-\<ZZ> code: 0x002128 group: letter
-\<aa> code: 0x01d51e group: letter
-\<bb> code: 0x01d51f group: letter
-\<cc> code: 0x01d520 group: letter
-\<dd> code: 0x01d521 group: letter
-\<ee> code: 0x01d522 group: letter
-\<ff> code: 0x01d523 group: letter
-\<gg> code: 0x01d524 group: letter
-\<hh> code: 0x01d525 group: letter
-\<ii> code: 0x01d526 group: letter
-\<jj> code: 0x01d527 group: letter
-\<kk> code: 0x01d528 group: letter
-\<ll> code: 0x01d529 group: letter
-\<mm> code: 0x01d52a group: letter
-\<nn> code: 0x01d52b group: letter
-\<oo> code: 0x01d52c group: letter
-\<pp> code: 0x01d52d group: letter
-\<qq> code: 0x01d52e group: letter
-\<rr> code: 0x01d52f group: letter
-\<ss> code: 0x01d530 group: letter
-\<tt> code: 0x01d531 group: letter
-\<uu> code: 0x01d532 group: letter
-\<vv> code: 0x01d533 group: letter
-\<ww> code: 0x01d534 group: letter
-\<xx> code: 0x01d535 group: letter
-\<yy> code: 0x01d536 group: letter
-\<zz> code: 0x01d537 group: letter
-\<alpha> code: 0x0003b1 group: greek
-\<beta> code: 0x0003b2 group: greek
-\<gamma> code: 0x0003b3 group: greek
-\<delta> code: 0x0003b4 group: greek
-\<epsilon> code: 0x0003b5 group: greek
-\<zeta> code: 0x0003b6 group: greek
-\<eta> code: 0x0003b7 group: greek
-\<theta> code: 0x0003b8 group: greek
-\<iota> code: 0x0003b9 group: greek
-\<kappa> code: 0x0003ba group: greek
-\<lambda> code: 0x0003bb group: greek abbrev: %
-\<mu> code: 0x0003bc group: greek
-\<nu> code: 0x0003bd group: greek
-\<xi> code: 0x0003be group: greek
-\<pi> code: 0x0003c0 group: greek
-\<rho> code: 0x0003c1 group: greek
-\<sigma> code: 0x0003c3 group: greek
-\<tau> code: 0x0003c4 group: greek
-\<upsilon> code: 0x0003c5 group: greek
-\<phi> code: 0x0003c6 group: greek
-\<chi> code: 0x0003c7 group: greek
-\<psi> code: 0x0003c8 group: greek
-\<omega> code: 0x0003c9 group: greek
-\<Gamma> code: 0x000393 group: greek
-\<Delta> code: 0x000394 group: greek
-\<Theta> code: 0x000398 group: greek
-\<Lambda> code: 0x00039b group: greek
-\<Xi> code: 0x00039e group: greek
-\<Pi> code: 0x0003a0 group: greek
-\<Sigma> code: 0x0003a3 group: greek
-\<Upsilon> code: 0x0003a5 group: greek
-\<Phi> code: 0x0003a6 group: greek
-\<Psi> code: 0x0003a8 group: greek
-\<Omega> code: 0x0003a9 group: greek
-\<bool> code: 0x01d539 group: letter
-\<complex> code: 0x002102 group: letter
-\<nat> code: 0x002115 group: letter
-\<rat> code: 0x00211a group: letter
-\<real> code: 0x00211d group: letter
-\<int> code: 0x002124 group: letter
-\<leftarrow> code: 0x002190 group: arrow
-\<longleftarrow> code: 0x0027f5 group: arrow
-\<rightarrow> code: 0x002192 group: arrow abbrev: ->
-\<longrightarrow> code: 0x0027f6 group: arrow abbrev: -->
-\<Leftarrow> code: 0x0021d0 group: arrow
-\<Longleftarrow> code: 0x0027f8 group: arrow
-\<Rightarrow> code: 0x0021d2 group: arrow abbrev: =>
-\<Longrightarrow> code: 0x0027f9 group: arrow abbrev: ==>
-\<leftrightarrow> code: 0x002194 group: arrow
-\<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <->
-\<Leftrightarrow> code: 0x0021d4 group: arrow
-\<Longleftrightarrow> code: 0x0027fa group: arrow abbrev: <=>
-\<mapsto> code: 0x0021a6 group: arrow abbrev: |->
-\<longmapsto> code: 0x0027fc group: arrow abbrev: |-->
-\<midarrow> code: 0x002500 group: arrow
-\<Midarrow> code: 0x002550 group: arrow
-\<hookleftarrow> code: 0x0021a9 group: arrow
-\<hookrightarrow> code: 0x0021aa group: arrow
-\<leftharpoondown> code: 0x0021bd group: arrow
-\<rightharpoondown> code: 0x0021c1 group: arrow
-\<leftharpoonup> code: 0x0021bc group: arrow
-\<rightharpoonup> code: 0x0021c0 group: arrow
-\<rightleftharpoons> code: 0x0021cc group: arrow
-\<leadsto> code: 0x00219d group: arrow abbrev: ~>
-\<downharpoonleft> code: 0x0021c3 group: arrow
-\<downharpoonright> code: 0x0021c2 group: arrow
-\<upharpoonleft> code: 0x0021bf group: arrow
-#\<upharpoonright> code: 0x0021be group: arrow
-\<restriction> code: 0x0021be group: punctuation
-\<Colon> code: 0x002237 group: punctuation
-\<up> code: 0x002191 group: arrow
-\<Up> code: 0x0021d1 group: arrow
-\<down> code: 0x002193 group: arrow
-\<Down> code: 0x0021d3 group: arrow
-\<updown> code: 0x002195 group: arrow
-\<Updown> code: 0x0021d5 group: arrow
-\<langle> code: 0x0027e8 group: punctuation abbrev: <.
-\<rangle> code: 0x0027e9 group: punctuation abbrev: .>
-\<lceil> code: 0x002308 group: punctuation
-\<rceil> code: 0x002309 group: punctuation
-\<lfloor> code: 0x00230a group: punctuation
-\<rfloor> code: 0x00230b group: punctuation
-\<lparr> code: 0x002987 group: punctuation abbrev: (|
-\<rparr> code: 0x002988 group: punctuation abbrev: |)
-\<lbrakk> code: 0x0027e6 group: punctuation abbrev: [|
-\<rbrakk> code: 0x0027e7 group: punctuation abbrev: |]
-\<lbrace> code: 0x002983 group: punctuation abbrev: {.
-\<rbrace> code: 0x002984 group: punctuation abbrev: .}
-\<guillemotleft> code: 0x0000ab group: punctuation abbrev: <<
-\<guillemotright> code: 0x0000bb group: punctuation abbrev: >>
-\<bottom> code: 0x0022a5 group: logic
-\<top> code: 0x0022a4 group: logic
-\<and> code: 0x002227 group: logic abbrev: /\
-\<And> code: 0x0022c0 group: logic abbrev: !!
-\<or> code: 0x002228 group: logic abbrev: \/
-\<Or> code: 0x0022c1 group: logic abbrev: ??
-\<forall> code: 0x002200 group: logic abbrev: !
-\<exists> code: 0x002203 group: logic abbrev: ?
-\<nexists> code: 0x002204 group: logic abbrev: ~?
-\<not> code: 0x0000ac group: logic abbrev: ~
-\<box> code: 0x0025a1 group: logic
-\<diamond> code: 0x0025c7 group: logic
-\<turnstile> code: 0x0022a2 group: relation abbrev: |-
-\<Turnstile> code: 0x0022a8 group: relation abbrev: |=
-\<tturnstile> code: 0x0022a9 group: relation abbrev: ||-
-\<TTurnstile> code: 0x0022ab group: relation abbrev: ||=
-\<stileturn> code: 0x0022a3 group: relation abbrev: -|
-\<surd> code: 0x00221a group: relation
-\<le> code: 0x002264 group: relation abbrev: <=
-\<ge> code: 0x002265 group: relation abbrev: >=
-\<lless> code: 0x00226a group: relation
-\<ggreater> code: 0x00226b group: relation
-\<lesssim> code: 0x002272 group: relation
-\<greatersim> code: 0x002273 group: relation
-\<lessapprox> code: 0x002a85 group: relation
-\<greaterapprox> code: 0x002a86 group: relation
-\<in> code: 0x002208 group: relation abbrev: :
-\<notin> code: 0x002209 group: relation abbrev: ~:
-\<subset> code: 0x002282 group: relation
-\<supset> code: 0x002283 group: relation
-\<subseteq> code: 0x002286 group: relation abbrev: (=
-\<supseteq> code: 0x002287 group: relation abbrev: =)
-\<sqsubset> code: 0x00228f group: relation
-\<sqsupset> code: 0x002290 group: relation
-\<sqsubseteq> code: 0x002291 group: relation abbrev: [=
-\<sqsupseteq> code: 0x002292 group: relation abbrev: =]
-\<inter> code: 0x002229 group: operator
-\<Inter> code: 0x0022c2 group: operator
-\<union> code: 0x00222a group: operator
-\<Union> code: 0x0022c3 group: operator
-\<squnion> code: 0x002294 group: operator
-\<Squnion> code: 0x002a06 group: operator
-\<sqinter> code: 0x002293 group: operator
-\<Sqinter> code: 0x002a05 group: operator
-\<setminus> code: 0x002216 group: operator
-\<propto> code: 0x00221d group: operator
-\<uplus> code: 0x00228e group: operator
-\<Uplus> code: 0x002a04 group: operator
-\<noteq> code: 0x002260 group: relation abbrev: ~=
-\<sim> code: 0x00223c group: relation
-\<doteq> code: 0x002250 group: relation
-\<simeq> code: 0x002243 group: relation
-\<approx> code: 0x002248 group: relation
-\<asymp> code: 0x00224d group: relation
-\<cong> code: 0x002245 group: relation
-\<smile> code: 0x002323 group: relation
-\<equiv> code: 0x002261 group: relation abbrev: ==
-\<frown> code: 0x002322 group: relation
-\<Join> code: 0x0022c8
-\<bowtie> code: 0x002a1d
-\<prec> code: 0x00227a group: relation
-\<succ> code: 0x00227b group: relation
-\<preceq> code: 0x00227c group: relation
-\<succeq> code: 0x00227d group: relation
-\<parallel> code: 0x002225 group: punctuation abbrev: ||
-\<bar> code: 0x0000a6 group: punctuation
-\<plusminus> code: 0x0000b1 group: operator
-\<minusplus> code: 0x002213 group: operator
-\<times> code: 0x0000d7 group: operator
-\<div> code: 0x0000f7 group: operator
-\<cdot> code: 0x0022c5 group: operator
-\<star> code: 0x0022c6 group: operator
-\<bullet> code: 0x002219 group: operator
-\<circ> code: 0x002218 group: operator
-\<dagger> code: 0x002020
-\<ddagger> code: 0x002021
-\<lhd> code: 0x0022b2 group: relation
-\<rhd> code: 0x0022b3 group: relation
-\<unlhd> code: 0x0022b4 group: relation
-\<unrhd> code: 0x0022b5 group: relation
-\<triangleleft> code: 0x0025c3 group: relation
-\<triangleright> code: 0x0025b9 group: relation
-\<triangle> code: 0x0025b3 group: relation
-\<triangleq> code: 0x00225c group: relation
-\<oplus> code: 0x002295 group: operator abbrev: +o
-\<Oplus> code: 0x002a01 group: operator abbrev: +O
-\<otimes> code: 0x002297 group: operator abbrev: *o
-\<Otimes> code: 0x002a02 group: operator abbrev: *O
-\<odot> code: 0x002299 group: operator abbrev: .o
-\<Odot> code: 0x002a00 group: operator abbrev: .O
-\<ominus> code: 0x002296 group: operator abbrev: -o
-\<oslash> code: 0x002298 group: operator abbrev: /o
-\<dots> code: 0x002026 group: punctuation abbrev: ...
-\<cdots> code: 0x0022ef group: punctuation
-\<Sum> code: 0x002211 group: operator abbrev: SUM
-\<Prod> code: 0x00220f group: operator abbrev: PROD
-\<Coprod> code: 0x002210 group: operator
-\<infinity> code: 0x00221e
-\<integral> code: 0x00222b group: operator
-\<ointegral> code: 0x00222e group: operator
-\<clubsuit> code: 0x002663
-\<diamondsuit> code: 0x002662
-\<heartsuit> code: 0x002661
-\<spadesuit> code: 0x002660
-\<aleph> code: 0x002135
-\<emptyset> code: 0x002205
-\<nabla> code: 0x002207
-\<partial> code: 0x002202
-\<flat> code: 0x00266d
-\<natural> code: 0x00266e
-\<sharp> code: 0x00266f
-\<angle> code: 0x002220
-\<copyright> code: 0x0000a9
-\<registered> code: 0x0000ae
-\<hyphen> code: 0x0000ad group: punctuation
-\<inverse> code: 0x0000af group: punctuation
-\<onequarter> code: 0x0000bc group: digit
-\<onehalf> code: 0x0000bd group: digit
-\<threequarters> code: 0x0000be group: digit
-\<ordfeminine> code: 0x0000aa
-\<ordmasculine> code: 0x0000ba
-\<section> code: 0x0000a7
-\<paragraph> code: 0x0000b6
-\<exclamdown> code: 0x0000a1
-\<questiondown> code: 0x0000bf
-\<euro> code: 0x0020ac
-\<pounds> code: 0x0000a3
-\<yen> code: 0x0000a5
-\<cent> code: 0x0000a2
-\<currency> code: 0x0000a4
-\<degree> code: 0x0000b0
-\<amalg> code: 0x002a3f group: operator
-\<mho> code: 0x002127 group: operator
-\<lozenge> code: 0x0025ca
-\<wp> code: 0x002118
-\<wrong> code: 0x002240 group: relation
-\<struct> code: 0x0022c4
-\<acute> code: 0x0000b4
-\<index> code: 0x000131
-\<dieresis> code: 0x0000a8
-\<cedilla> code: 0x0000b8
-\<hungarumlaut> code: 0x0002dd
-\<some> code: 0x0003f5
-\<^sub> code: 0x0021e9 group: control font: IsabelleText
-\<^sup> code: 0x0021e7 group: control font: IsabelleText
-\<^bold> code: 0x002759 group: control font: IsabelleText
-\<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(
-\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)
-\<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^(
-\<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^)
-
--- a/src/Tools/WWW_Find/find_theorems.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* Title: Tools/WWW_Find/find_theorems.ML
- Author: Timothy Bourke, NICTA
-
-Simple find_theorems server.
-*)
-
-local
-
-val default_limit = 20;
-val all_thy_names = sort string_ord (Thy_Info.get_names ());
-
-fun app_index f xs = fold_index (fn x => K (f x)) xs ();
-
-fun find_theorems arg_data send =
- let
- val args = Symtab.lookup arg_data;
-
- val query_str = the_default "" (args "query");
- fun get_query () = Find_Theorems.read_query Position.none query_str;
-
- val limit = case args "limit" of
- NONE => default_limit
- | SOME str => the_default default_limit (Int.fromString str);
- val thy_name = the_default "Main" (args "theory");
- val with_dups = is_some (args "with_dups");
-
- val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
-
- fun do_find query =
- let
- val (othmslen, thms) =
- Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
- ||> rev;
- in
- Xhtml.write send
- (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
- if null thms then ()
- else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
- HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
- end;
- in
- send Xhtml.doctype_xhtml1_0_strict;
- Xhtml.write_enclosed send
- (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
- (fn send =>
- if query_str = "" then ()
- else
- do_find (get_query ())
- handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
- end;
-in
-
-val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
-
-end;
-
--- a/src/Tools/WWW_Find/html_templates.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-(* Title: Tools/WWW_Find/html_templates.ML
- Author: Timothy Bourke, NICTA
-
-HTML Templates for find theorems server.
-*)
-
-signature HTML_TEMPLATES =
-sig
- val find_theorems_form: string -> (string option * int * bool * string list) -> Xhtml.tag
-
- val header: string -> (string option * int * bool * string list) -> Xhtml.tag
- val error: string -> Xhtml.tag
- val find_theorems_table: Xhtml.tag
-
- val find_theorems_summary: int option * int * string Symtab.table -> Xhtml.tag
- val html_thm: Proof.context -> (int * (Facts.ref * thm)) -> Xhtml.tag
-end
-
-
-structure HTML_Templates: HTML_TEMPLATES =
-struct
-
-open Xhtml;
-
-fun find_theorems_form thy_name (query, limit, withdups, all_thy_names) =
- 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 (string_of_int limit),
- maxlength = NONE }})
- ];
-
- val theories = divele noid
- [
- label (noid, { for = "theory" }, "Search in:"),
- select (id "theory", { name = "theory", value = SOME thy_name })
- all_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 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 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;
- in
- (case c of
- Find_Theorems.Name name => prfx ("name: " ^ quote name)
- | Find_Theorems.Intro => prfx "intro"
- | 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, args) =
- let
- val args =
- (case othmslen of
- NONE => args
- | SOME l => Symtab.update ("limit", string_of_int l) args)
- val qargs = HttpUtil.make_query_string args;
-
- val num_found_text =
- (case othmslen of
- NONE => text (string_of_int thmslen)
- | SOME l =>
- a { href = "find_theorems" ^
- (if qargs = "" then "" else "?" ^ qargs),
- text = string_of_int l })
- val found = [text "found ", num_found_text, text " theorems"] : tag list;
- val displayed =
- if is_some othmslen
- then " (" ^ string_of_int thmslen ^ " displayed)"
- else "";
- in
- table (class "findtheoremsquery")
- [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
- end
-
-(* FIXME!?! *)
-fun is_sorry thm =
- Thm.proof_of thm
- |> Proofterm.approximate_proof_body
- |> Proofterm.all_oracles_of
- |> exists (fn (x, _) => x = "Pure.skip_proof");
-
-fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
-
-fun html_thm ctxt (n, (thmref, thm)) =
- let
- val output_thm =
- Output.output o Pretty.string_of_margin 100 o
- Display.pretty_thm (Config.put show_question_marks false ctxt);
- in
- tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
- [
- tag' "td" (class "name")
- [span' (sorry_class thm)
- [raw_text (Facts.string_of_ref thmref)]
- ],
- tag' "td" (class "thm") [pre noid (output_thm thm)]
- ]
- end;
-
-end;
-
-
--- a/src/Tools/WWW_Find/html_unicode.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: Tools/WWW_Find/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 = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
-
-(* symbol output *)
-
-local
- val sym_width_lookup = Symtab.make
- [("\<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, "&#" ^ string_of_int 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_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
- | output_syms ("\<^sup>" :: s :: ss) = output_sup 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;
--- a/src/Tools/WWW_Find/http_status.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-(* Title: Tools/WWW_Find/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;
-
--- a/src/Tools/WWW_Find/http_util.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(* Title: Tools/WWW_Find/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) = implode [name, ": ", value, crlf];
-
-fun reply_header (status, content_type, extra_fields) =
- let
- val code = (string_of_int o HttpStatus.to_status_code) status;
- val reason = HttpStatus.to_reason status;
- val show_content_type = pair "Content-Type" o Mime.show_type;
- in
- implode
- (map make_header_field
- (("Status", implode [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.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 General.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
- #> space_implode "&";
-
-end;
-
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-#!/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 checkplatform()
-{
- case "$ISABELLE_PLATFORM" in
- *-linux)
- ;;
- *)
- fail "Platform $ISABELLE_PLATFORM currently not supported by $PRG component"
- ;;
- esac
-}
-
-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 "
-}
-
-## platform support check
-
-checkplatform
-
-## 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"`
-
-# inform theory which SCGI port to use via environment variable
-export SCGIPORT
-MLSTARTSERVER="use_thy \"Start_WWW_Find\";"
-
-case "$COMMAND" in
- start)
- "$LIGHTTPD" -f "$WWWCONFIG"
- if [ "$LOGFILE" = true ]; then
- (cd "$WWWFINDDIR"; \
- nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" "$INPUT") &
- else
- (cd "$WWWFINDDIR"; \
- nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -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
-
--- a/src/Tools/WWW_Find/lighttpd.conf Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-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"
- )))
-
--- a/src/Tools/WWW_Find/mime.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* Title: Tools/WWW_Find/mime.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) = implode ["; ", n, "=", v];
-
-fun show_type (Type {main, sub, params}) =
- implode ([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;
-
--- a/src/Tools/WWW_Find/scgi_req.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,161 +0,0 @@
-(* Title: Tools/WWW_Find/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 " ^ string_of_int 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 =
- (case Int.fromString (field "CONTENT_LENGTH") of
- SOME n => n
- | NONE => 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
- implode
- (["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;
-
--- a/src/Tools/WWW_Find/scgi_server.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: Tools/WWW_Find/scgi_server.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 *)
- val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
- val raw_post_handler : (string -> string) -> handler
-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 = Socket_Util.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 (* FIXME avoid low-level Poly/ML thread primitives *)
- (fn () => Runtime.exn_trace threadf,
- [Thread.EnableBroadcastInterrupt true,
- Thread.InterruptState
- Thread.InterruptAsynchOnce])))
- end;
-
- fun loop () =
- let
- val (sock, _)= Socket.accept passive_sock;
-
- val (sin, sout) = Socket_Util.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 () = (* FIXME avoid handle e *)
- (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 on port " ^ string_of_int port ^ ".");
- 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 "
- ^ string_of_int port ^ ". Trying again in "
- ^ string_of_int delay ^ " seconds...");
- OS.Process.sleep (Time.fromSeconds delay);
- server' (countdown - 1) server_prefix port);
-end;
-
-fun simple_handler h (ScgiReq.Req {request_method, query_string, ...}, content, send) =
- h (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.")
- send;
-
-fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
- send (h (Byte.bytesToString content))
- | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
-
-end;
-
--- a/src/Tools/WWW_Find/socket_util.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-(* Title: Tools/WWW_Find/socket_util.ML
- Author: Timothy Bourke, NICTA
-
-Routines for working with sockets. Following example 10.2 in "The
-Standard-ML Basis Library" by Emden R. Gansner and John H. Reppy.
-*)
-
-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 Socket_Util: SOCKET_UTIL =
-struct
-
-fun init_server_socket opt_host port =
- let
- val sock = INetSock.TCP.socket ();
- val addr =
- (case opt_host of
- NONE => INetSock.any port
- | SOME host =>
- NetHostDB.getByName host
- |> the
- |> NetHostDB.addr
- |> rpair port
- |> INetSock.toAddr
- handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host));
- val _ = Socket.bind (sock, addr);
- val _ = Socket.listen (sock, 5);
- in sock end;
-
-fun make_streams sock =
- let
- val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
-
- val sock_name =
- implode [ NetHostDB.toString haddr, ":", string_of_int 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;
-
--- a/src/Tools/WWW_Find/unicode_symbols.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,279 +0,0 @@
-(* Title: Tools/WWW_Find/unicode_symbols.ML
- Author: Timothy Bourke, NICTA
-
-Parsing of private etc/symbols.
-*)
-
-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", "group", "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_Pos.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_Pos.symbol)
- -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
- >> (token AsciiSymbol o op ::);
-
-fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
-val scan_comment =
- $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
- >> token Comment;
-
-fun is_sym s =
- (case Symbol.decode s of
- Symbol.Sym _ => true
- | Symbol.Ctrl _ => true
- | _ => false);
-
-fun tokenize syms =
- let
- val scanner =
- Scan.one (is_sym o Symbol_Pos.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.!!! (fn () => "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.here (#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 *)
-
-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 group = Scan.option ($$$ "group" -- $$$ ":" |-- name);
-val font = Scan.option ($$$ "font" -- $$$ ":" |-- name);
-val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
- |-- (ascii_sym || $$$ ":" || name));
-
-in
-
-val line = (symbol -- unicode -- group -- font -- abbr)
- >> (fn ((((a, b), _), _), c) => (a, b, c));
-
-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.here pos)
- | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos);
-
-in
-
-fun read_symbols path =
- let
- val parsed_lines =
- Symbol_Pos.explode (File.read path, Path.position 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 @{path "~~/src/Tools/WWW_Find/etc/symbols"};
-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;
-
--- a/src/Tools/WWW_Find/www/basic.css Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-
-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;
-}
-
--- a/src/Tools/WWW_Find/www/find_theorems.js Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,406 +0,0 @@
-/*
- * 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['\\<II>'] = 'โ';
-utf8['\\<VV>'] = '๐';
-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['\\<RR>'] = 'โ';
-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['\\<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['\\<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['\\<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);
- }
-}
-
--- a/src/Tools/WWW_Find/www/pasting_help.html Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-<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 with x-symbol</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>
-
--- a/src/Tools/WWW_Find/xhtml.ML Sat Apr 26 06:43:06 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,441 +0,0 @@
-(* Title: Tools/WWW_Find/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_enclosed: (string -> unit) -> tag -> ((string -> unit) -> unit) -> 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) = implode [" ", 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 flat (
- [[">"]]
- @
- 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 write_enclosed pr template content =
- (write_open pr template; content pr; write_close pr template)
-
-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 string_of_int);
-
-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" ^ string_of_int 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, maps 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", string_of_int 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;
-