# HG changeset patch # User kleing # Date 1398512229 -36000 # Node ID 13b0fc4ece4240147c56688d13cc57929353c652 # Parent e4f363e16bdc84f1f84b50867cef730a6765d609 retired wwwfind diff -r e4f363e16bdc -r 13b0fc4ece42 NEWS --- 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) ------------------------------------- diff -r e4f363e16bdc -r 13b0fc4ece42 etc/components --- 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 diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/ROOT --- 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 diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/Start_WWW_Find.thy --- 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 - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/WWW_Find.thy --- 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 - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/doc/README --- 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 - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/doc/design.tex --- 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+\+. -The existing Thy/Html module in the Isabelle Pure theory converts many of -these symbols to \ac{HTML} entities. -Custom routines are required to convert the missing symbols to \ac{HTML} -\emph{numeric character references}, which are the Unicode codepoints of -symbols printed in decimal between \verb+&#+ and \verb+;+. -Further, other routines were required for converting \acs{UTF-8} encoded -strings sent from web browsers into Isabelle's symbol encoding. - -Isabelle is distributed with a text file that maps Isabelle symbols to -Unicode codepoints. -A module was written to parse this file into symbol tables that map back and -forth between Isabelle symbols and Unicode codepoints, and also between -Isabelle \acs{ASCII} abbreviations (like \verb+-->+ for $\longrightarrow$) -and Unicode codepoints. - -The conversion from Isabelle symbols to \ac{HTML} numeric character -references is handled by a new printing mode, which is based in large part -on the existing \ac{HTML} printing mode. -The new mode is used in combination with the existing \texttt{xsymbol} mode, -to ensure that Isabelle symbols are used instead of \acs{ASCII} -abbreviations. - -The conversion from \acs{UTF-8} is handled by a custom routine. -Additionally, there is a JavaScript routine that converts from Isabelle -symbol encodings to \acs{UTF-8}, so that users can conveniently view -manually-entered or pasted mathematical characters in the web browser -interface. - -\section{Abbreviations}\label{sec:abbr} - -\begin{acronym}[SML/NJ] % longest acronym here - \acro{ASCII}{American Standard Code for Information Interchange} - \acro{CGI}{Common Gateway Interface} - \acro{CML}{Concurrent ML} - \acro{CMU}{Carnegie Mellon University} - \acro{HTML}{Hyper Text Markup Language} - \acro{HTTP}{Hyper Text Transfer Protocol} - \acro{ML}{Meta Language} - \acro{SCGI}{Simple CGI} - \acro{SML}{Standard ML} - \acro{SML/NJ}{Standard ML of New Jersey} - \acro{URL}{Universal Resource Locator} - \acro{UTF-8}{8-bit Unicode Transformation Format} - \acro{WWW}{World Wide Web} -\end{acronym} - -\end{document} diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/echo.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/etc/settings --- 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" diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/etc/symbols --- 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) - -\ code: 0x01d7ec group: digit -\ code: 0x01d7ed group: digit -\ code: 0x01d7ee group: digit -\ code: 0x01d7ef group: digit -\ code: 0x01d7f0 group: digit -\ code: 0x01d7f1 group: digit -\ code: 0x01d7f2 group: digit -\ code: 0x01d7f3 group: digit -\ code: 0x01d7f4 group: digit -\ code: 0x01d7f5 group: digit -\ code: 0x01d49c group: letter -\ code: 0x00212c group: letter -\ code: 0x01d49e group: letter -\ code: 0x01d49f group: letter -\ code: 0x002130 group: letter -\ code: 0x002131 group: letter -\ code: 0x01d4a2 group: letter -\ code: 0x00210b group: letter -\ code: 0x002110 group: letter -\ code: 0x01d4a5 group: letter -\ code: 0x01d4a6 group: letter -\ code: 0x002112 group: letter -\ code: 0x002133 group: letter -\ code: 0x01d4a9 group: letter -\ code: 0x01d4aa group: letter -\

code: 0x01d5c9 group: letter -\ code: 0x01d5ca group: letter -\ code: 0x01d5cb group: letter -\ code: 0x01d5cc group: letter -\ code: 0x01d5cd group: letter -\ code: 0x01d5ce group: letter -\ code: 0x01d5cf group: letter -\ code: 0x01d5d0 group: letter -\ code: 0x01d5d1 group: letter -\ code: 0x01d5d2 group: letter -\ code: 0x01d5d3 group: letter -\ code: 0x01d504 group: letter -\ code: 0x01d505 group: letter -\ code: 0x00212d group: letter -\

code: 0x01d507 group: letter -\ code: 0x01d508 group: letter -\ code: 0x01d509 group: letter -\ code: 0x01d50a group: letter -\ code: 0x00210c group: letter -\ code: 0x002111 group: letter -\ code: 0x01d50d group: letter -\ code: 0x01d50e group: letter -\ code: 0x01d50f group: letter -\ code: 0x01d510 group: letter -\ code: 0x01d511 group: letter -\ code: 0x01d512 group: letter -\ code: 0x01d513 group: letter -\ code: 0x01d514 group: letter -\ code: 0x00211c group: letter -\ code: 0x01d516 group: letter -\ code: 0x01d517 group: letter -\ code: 0x01d518 group: letter -\ code: 0x01d519 group: letter -\ code: 0x01d51a group: letter -\ code: 0x01d51b group: letter -\ code: 0x01d51c group: letter -\ code: 0x002128 group: letter -\ code: 0x01d51e group: letter -\ code: 0x01d51f group: letter -\ code: 0x01d520 group: letter -\
code: 0x01d521 group: letter -\ code: 0x01d522 group: letter -\ code: 0x01d523 group: letter -\ code: 0x01d524 group: letter -\ code: 0x01d525 group: letter -\ code: 0x01d526 group: letter -\ code: 0x01d527 group: letter -\ code: 0x01d528 group: letter -\ code: 0x01d529 group: letter -\ code: 0x01d52a group: letter -\ code: 0x01d52b group: letter -\ code: 0x01d52c group: letter -\ code: 0x01d52d group: letter -\ code: 0x01d52e group: letter -\ code: 0x01d52f group: letter -\ code: 0x01d530 group: letter -\ code: 0x01d531 group: letter -\ code: 0x01d532 group: letter -\ code: 0x01d533 group: letter -\ code: 0x01d534 group: letter -\ code: 0x01d535 group: letter -\ code: 0x01d536 group: letter -\ code: 0x01d537 group: letter -\ code: 0x0003b1 group: greek -\ code: 0x0003b2 group: greek -\ code: 0x0003b3 group: greek -\ code: 0x0003b4 group: greek -\ code: 0x0003b5 group: greek -\ code: 0x0003b6 group: greek -\ code: 0x0003b7 group: greek -\ code: 0x0003b8 group: greek -\ code: 0x0003b9 group: greek -\ code: 0x0003ba group: greek -\ code: 0x0003bb group: greek abbrev: % -\ code: 0x0003bc group: greek -\ code: 0x0003bd group: greek -\ code: 0x0003be group: greek -\ code: 0x0003c0 group: greek -\ code: 0x0003c1 group: greek -\ code: 0x0003c3 group: greek -\ code: 0x0003c4 group: greek -\ code: 0x0003c5 group: greek -\ code: 0x0003c6 group: greek -\ code: 0x0003c7 group: greek -\ code: 0x0003c8 group: greek -\ code: 0x0003c9 group: greek -\ code: 0x000393 group: greek -\ code: 0x000394 group: greek -\ code: 0x000398 group: greek -\ code: 0x00039b group: greek -\ code: 0x00039e group: greek -\ code: 0x0003a0 group: greek -\ code: 0x0003a3 group: greek -\ code: 0x0003a5 group: greek -\ code: 0x0003a6 group: greek -\ code: 0x0003a8 group: greek -\ code: 0x0003a9 group: greek -\ code: 0x01d539 group: letter -\ code: 0x002102 group: letter -\ code: 0x002115 group: letter -\ code: 0x00211a group: letter -\ code: 0x00211d group: letter -\ code: 0x002124 group: letter -\ code: 0x002190 group: arrow -\ code: 0x0027f5 group: arrow -\ code: 0x002192 group: arrow abbrev: -> -\ code: 0x0027f6 group: arrow abbrev: --> -\ code: 0x0021d0 group: arrow -\ code: 0x0027f8 group: arrow -\ code: 0x0021d2 group: arrow abbrev: => -\ code: 0x0027f9 group: arrow abbrev: ==> -\ code: 0x002194 group: arrow -\ code: 0x0027f7 group: arrow abbrev: <-> -\ code: 0x0021d4 group: arrow -\ code: 0x0027fa group: arrow abbrev: <=> -\ code: 0x0021a6 group: arrow abbrev: |-> -\ code: 0x0027fc group: arrow abbrev: |--> -\ code: 0x002500 group: arrow -\ code: 0x002550 group: arrow -\ code: 0x0021a9 group: arrow -\ code: 0x0021aa group: arrow -\ code: 0x0021bd group: arrow -\ code: 0x0021c1 group: arrow -\ code: 0x0021bc group: arrow -\ code: 0x0021c0 group: arrow -\ code: 0x0021cc group: arrow -\ code: 0x00219d group: arrow abbrev: ~> -\ code: 0x0021c3 group: arrow -\ code: 0x0021c2 group: arrow -\ code: 0x0021bf group: arrow -#\ code: 0x0021be group: arrow -\ code: 0x0021be group: punctuation -\ code: 0x002237 group: punctuation -\ code: 0x002191 group: arrow -\ code: 0x0021d1 group: arrow -\ code: 0x002193 group: arrow -\ code: 0x0021d3 group: arrow -\ code: 0x002195 group: arrow -\ code: 0x0021d5 group: arrow -\ code: 0x0027e8 group: punctuation abbrev: <. -\ code: 0x0027e9 group: punctuation abbrev: .> -\ code: 0x002308 group: punctuation -\ code: 0x002309 group: punctuation -\ code: 0x00230a group: punctuation -\ code: 0x00230b group: punctuation -\ code: 0x002987 group: punctuation abbrev: (| -\ code: 0x002988 group: punctuation abbrev: |) -\ code: 0x0027e6 group: punctuation abbrev: [| -\ code: 0x0027e7 group: punctuation abbrev: |] -\ code: 0x002983 group: punctuation abbrev: {. -\ code: 0x002984 group: punctuation abbrev: .} -\ code: 0x0000ab group: punctuation abbrev: << -\ code: 0x0000bb group: punctuation abbrev: >> -\ code: 0x0022a5 group: logic -\ code: 0x0022a4 group: logic -\ code: 0x002227 group: logic abbrev: /\ -\ code: 0x0022c0 group: logic abbrev: !! -\ code: 0x002228 group: logic abbrev: \/ -\ code: 0x0022c1 group: logic abbrev: ?? -\ code: 0x002200 group: logic abbrev: ! -\ code: 0x002203 group: logic abbrev: ? -\ code: 0x002204 group: logic abbrev: ~? -\ code: 0x0000ac group: logic abbrev: ~ -\ code: 0x0025a1 group: logic -\ code: 0x0025c7 group: logic -\ code: 0x0022a2 group: relation abbrev: |- -\ code: 0x0022a8 group: relation abbrev: |= -\ code: 0x0022a9 group: relation abbrev: ||- -\ code: 0x0022ab group: relation abbrev: ||= -\ code: 0x0022a3 group: relation abbrev: -| -\ code: 0x00221a group: relation -\ code: 0x002264 group: relation abbrev: <= -\ code: 0x002265 group: relation abbrev: >= -\ code: 0x00226a group: relation -\ code: 0x00226b group: relation -\ code: 0x002272 group: relation -\ code: 0x002273 group: relation -\ code: 0x002a85 group: relation -\ code: 0x002a86 group: relation -\ code: 0x002208 group: relation abbrev: : -\ code: 0x002209 group: relation abbrev: ~: -\ code: 0x002282 group: relation -\ code: 0x002283 group: relation -\ code: 0x002286 group: relation abbrev: (= -\ code: 0x002287 group: relation abbrev: =) -\ code: 0x00228f group: relation -\ code: 0x002290 group: relation -\ code: 0x002291 group: relation abbrev: [= -\ code: 0x002292 group: relation abbrev: =] -\ code: 0x002229 group: operator -\ code: 0x0022c2 group: operator -\ code: 0x00222a group: operator -\ code: 0x0022c3 group: operator -\ code: 0x002294 group: operator -\ code: 0x002a06 group: operator -\ code: 0x002293 group: operator -\ code: 0x002a05 group: operator -\ code: 0x002216 group: operator -\ code: 0x00221d group: operator -\ code: 0x00228e group: operator -\ code: 0x002a04 group: operator -\ code: 0x002260 group: relation abbrev: ~= -\ code: 0x00223c group: relation -\ code: 0x002250 group: relation -\ code: 0x002243 group: relation -\ code: 0x002248 group: relation -\ code: 0x00224d group: relation -\ code: 0x002245 group: relation -\ code: 0x002323 group: relation -\ code: 0x002261 group: relation abbrev: == -\ code: 0x002322 group: relation -\ code: 0x0022c8 -\ code: 0x002a1d -\ code: 0x00227a group: relation -\ code: 0x00227b group: relation -\ code: 0x00227c group: relation -\ code: 0x00227d group: relation -\ code: 0x002225 group: punctuation abbrev: || -\ code: 0x0000a6 group: punctuation -\ code: 0x0000b1 group: operator -\ code: 0x002213 group: operator -\ code: 0x0000d7 group: operator -\
code: 0x0000f7 group: operator -\ code: 0x0022c5 group: operator -\ code: 0x0022c6 group: operator -\ code: 0x002219 group: operator -\ code: 0x002218 group: operator -\ code: 0x002020 -\ code: 0x002021 -\ code: 0x0022b2 group: relation -\ code: 0x0022b3 group: relation -\ code: 0x0022b4 group: relation -\ code: 0x0022b5 group: relation -\ code: 0x0025c3 group: relation -\ code: 0x0025b9 group: relation -\ code: 0x0025b3 group: relation -\ code: 0x00225c group: relation -\ code: 0x002295 group: operator abbrev: +o -\ code: 0x002a01 group: operator abbrev: +O -\ code: 0x002297 group: operator abbrev: *o -\ code: 0x002a02 group: operator abbrev: *O -\ code: 0x002299 group: operator abbrev: .o -\ code: 0x002a00 group: operator abbrev: .O -\ code: 0x002296 group: operator abbrev: -o -\ code: 0x002298 group: operator abbrev: /o -\ code: 0x002026 group: punctuation abbrev: ... -\ code: 0x0022ef group: punctuation -\ code: 0x002211 group: operator abbrev: SUM -\ code: 0x00220f group: operator abbrev: PROD -\ code: 0x002210 group: operator -\ code: 0x00221e -\ code: 0x00222b group: operator -\ code: 0x00222e group: operator -\ code: 0x002663 -\ code: 0x002662 -\ code: 0x002661 -\ code: 0x002660 -\ code: 0x002135 -\ code: 0x002205 -\ code: 0x002207 -\ code: 0x002202 -\ code: 0x00266d -\ code: 0x00266e -\ code: 0x00266f -\ code: 0x002220 -\ code: 0x0000a9 -\ code: 0x0000ae -\ code: 0x0000ad group: punctuation -\ code: 0x0000af group: punctuation -\ code: 0x0000bc group: digit -\ code: 0x0000bd group: digit -\ code: 0x0000be group: digit -\ code: 0x0000aa -\ code: 0x0000ba -\
code: 0x0000a7 -\ code: 0x0000b6 -\ code: 0x0000a1 -\ code: 0x0000bf -\ code: 0x0020ac -\ code: 0x0000a3 -\ code: 0x0000a5 -\ code: 0x0000a2 -\ code: 0x0000a4 -\ code: 0x0000b0 -\ code: 0x002a3f group: operator -\ code: 0x002127 group: operator -\ code: 0x0025ca -\ code: 0x002118 -\ code: 0x002240 group: relation -\ code: 0x0022c4 -\ code: 0x0000b4 -\ code: 0x000131 -\ code: 0x0000a8 -\ code: 0x0000b8 -\ code: 0x0002dd -\ 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: =^) - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/find_theorems.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/html_templates.ML --- 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; - - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/html_unicode.ML --- 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 - [("\", 2), - ("\", 2), - ("\", 2), - ("\", 2), - ("\", 2), - ("\<^bsub>", 0), - ("\<^esub>", 0), - ("\<^bsup>", 0), - ("\<^esup>", 0)]; - - fun sym_width s = - (case Symtab.lookup sym_width_lookup s of - NONE => 1 - | SOME w => w); - - fun output_sym s = - if Symbol.is_raw s then (1, Symbol.decode_raw s) - else - (case UnicodeSymbols.symbol_to_unicode s of - SOME x => (sym_width s, "&#" ^ 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 "" "") (output_sym s); - fun output_sup s = apsnd (enclose "" "") (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 = ("", ""); - -val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name); - -end; diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/http_status.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/http_util.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/lib/Tools/wwwfind --- 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 - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/lighttpd.conf --- 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" - ))) - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/mime.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/scgi_req.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/scgi_server.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/socket_util.ML --- 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; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/unicode_symbols.ML --- 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 = "\"; - - fun word_to_symbol w = - (case (unicode_to_symbol o Word32.toInt) w of - NONE => "?" - | SOME s => s); - - fun andb32 (w1, w2) = - Word8.andb(w1, w2) - |> Word8.toLarge - |> Word32.fromLarge; - - fun read_next (ss, 0, c) = (word_to_symbol c, ss) - | read_next (ss, n, c) = - (case get_next ss of - NONE => (replacement_char, ss) - | SOME (w, ss') => - if Word8.andb (w, 0wxc0) <> 0wx80 - then (replacement_char, ss') - else - let - val w' = (Word8.andb (w, 0wx3f)); - val bw = (Word32.fromLarge o Word8.toLarge) w'; - val c' = Word32.<< (c, 0wx6); - in read_next (ss', n - 1, Word32.orb (c', bw)) end); - - fun do_char (w, ss) = - if Word8.andb (w, 0wx80) = 0wx00 - then (wstr w, ss) - else if Word8.andb (w, 0wx60) = 0wx40 - then read_next (ss, 1, andb32 (w, 0wx1f)) - else if Word8.andb (w, 0wxf0) = 0wxe0 - then read_next (ss, 2, andb32 (w, 0wx0f)) - else if Word8.andb (w, 0wxf8) = 0wxf0 - then read_next (ss, 3, andb32 (w, 0wx07)) - else (replacement_char, ss); - - fun read (rs, ss) = - (case Option.map do_char (get_next ss) of - NONE => (implode o rev) rs - | SOME (s, ss') => read (s::rs, ss')); - in read ([], Substring.full utf8str) end; - -local - -fun consec n = - fn w => ( - Word32.>> (w, Word.fromInt (n * 6)) - |> (curry Word32.andb) 0wx3f - |> (curry Word32.orb) 0wx80 - |> Word8.fromLargeWord o Word32.toLargeWord); - -fun stamp n = - fn w => ( - Word32.>> (w, Word.fromInt (n * 6)) - |> (curry Word32.andb) (Word32.>> (0wx000000ff, Word.fromInt (n + 2))) - |> (curry Word32.orb) (Word32.<< (0wxffffffff, Word.fromInt (7 - n))) - |> Word8.fromLargeWord o Word32.toLargeWord); - -fun to_utf8_bytes i = - if i <= 0x007f - then [Word8.fromInt i] - else let - val w = Word32.fromInt i; - in - if i < 0x07ff - then [stamp 1 w, consec 0 w] - else if i < 0xffff - then [stamp 2 w, consec 1 w, consec 0 w] - else if i < 0x10ffff - then [stamp 3 w, consec 2 w, consec 1 w, consec 0 w] - else [] - end; - -in - -fun utf8 is = - map to_utf8_bytes is - |> flat - |> Word8Vector.fromList - |> Byte.bytesToString; - -end - -end; - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/www/basic.css --- 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; -} - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/www/find_theorems.js --- 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['\\'] = 'โŠ‡'; -utf8['\\'] = '๐”Ž'; -utf8['\\'] = 'โ†‘'; -utf8['\\'] = 'โŠ—'; -utf8['\\'] = '๐”ž'; -utf8['\\'] = 'โ€ '; -utf8['\\'] = 'โŒข'; -utf8['\\'] = 'ยซ'; -utf8['\\'] = '๐”ฎ'; -utf8['\\'] = '๐’ณ'; -utf8['\\'] = 'โ–น'; -utf8['\\'] = 'ยป'; -utf8['\\'] = 'ฮฝ'; -utf8['\\'] = 'โˆผ'; -utf8['\\'] = 'โ‡'; -utf8['\\

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

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

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

'] = '๐”‡'; -utf8['\\'] = 'โˆ‰'; -utf8['\\'] = '๐—ƒ'; -utf8['\\'] = 'โŠŽ'; -utf8['\\'] = 'โ†”'; -utf8['\\'] = '๐”—'; -utf8['\\'] = 'โˆ™'; -utf8['\\'] = 'ฮ˜'; -utf8['\\'] = 'โŒฃ'; -utf8['\\'] = '๐’ข'; -utf8['\\'] = '๐”ง'; -utf8['\\'] = 'โˆฉ'; -utf8['\\'] = 'ฮจ'; -utf8['\\'] = 'ยช'; -utf8['\\'] = '๐’ฒ'; -utf8['\\'] = '๐”ท'; -utf8['\\'] = 'ฮธ'; -utf8['\\'] = 'ยบ'; -utf8['\\'] = '๐–ผ'; -utf8['\\'] = 'ฯˆ'; -utf8['\\'] = '๐—Œ'; -utf8['\\'] = 'โ‡”'; -utf8['\\'] = 'โ™ก'; -utf8['\\'] = '๐Ÿฐ'; - -var re_xsymbol = /\\<.*?>/g; - -function encodequery(ele) { - var text = ele.value; - var otext = text; - var pos = getCaret(ele); - - xsymbols = text.match(re_xsymbol); - for (i in xsymbols) { - var repl = utf8[xsymbols[i]]; - if (repl) { - text = text.replace(xsymbols[i], repl, "g"); - } - } - - if (text != otext) { - ele.value = text; - - if (pos != -1) { - pos = pos - (otext.length - text.length); - setCaret(ele, pos); - } - } -} - -/* from: http://www.webdeveloper.com/forum/showthread.php?t=74982 */ -function getCaret(obj) { - var pos = -1; - - if (document.selection) { // IE - obj.focus (); - var sel = document.selection.createRange(); - var sellen = document.selection.createRange().text.length; - sel.moveStart ('character', -obj.value.length); - pos = sel.text.length - sellen; - - } else if (obj.selectionStart || obj.selectionStart == '0') { // Gecko - pos = obj.selectionStart; - } - - return pos; -} - -/* from: http://parentnode.org/javascript/working-with-the-cursor-position/ */ -function setCaret(obj, pos) { - if (obj.createTextRange) { - var range = obj.createTextRange(); - range.move("character", pos); - range.select(); - } else if (obj.selectionStart) { - obj.focus(); - obj.setSelectionRange(pos, pos); - } -} - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/www/pasting_help.html --- 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 @@ - - - Find Theorems: help pasting from ProofGeneral - - - -

Pasting theory text from Proof General with x-symbol

-
    -
  1. Select the text using the keyboard (C-SPC, - arrow keys).
    2. -
  2. Choose X-Symbol/Other - Commands/Copy Encoded.
    3. -
  3. Paste into the web browser (C-v).
    4. -
- - Return to find_theorems - - - diff -r e4f363e16bdc -r 13b0fc4ece42 src/Tools/WWW_Find/xhtml.ML --- 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 - @ - [[""]] - ))); - -fun write pr = - let - fun f (Text t) = (pr o XML.text) t - | f (RawText t) = pr t - | f (Tag (nm, atts, inner)) = ( - pr "<"; - pr nm; - app (pr o show_att) atts; - if length inner = 0 - then pr "/>" - else ( - pr ">"; - app f inner; - pr ("") - )) - in f end; - -(* Print all opening tags down into the tree until a branch of degree > 1 is - found, in which case print everything before the last tag, which is then - opened. *) -fun write_open pr = - let - fun f (Text t) = (pr o XML.text) t - | f (RawText t) = pr t - | f (Tag (nm, atts, [])) = - (pr "<"; pr nm; app (pr o show_att) atts; pr ">") - | f (Tag (nm, atts, xs)) = - (pr "<"; pr nm; app (pr o show_att) atts; pr ">"; - (case take_suffix is_text xs of - ([], _) => () - | (b, _) => - let val (xs, x) = split_last b; - in app (write pr) xs; f x end)); - in f end; - -(* Print matching closing tags for write_open. *) -fun write_close pr = - let - fun close nm = pr (""); - val pr_text = app (pr o show_text); - - fun f (Text t) = () - | f (RawText t) = () - | f (Tag (nm, _, [])) = close nm - | f (Tag (nm, _, xs)) = - (case take_suffix is_text xs of - ([], text) => pr_text text - | (b, text) => - let val (xs, x) = split_last b; - in f x; close nm; pr_text text end); - in f end; - -fun 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 = - "\n"; - -end; -
'] = '๐”ก'; -utf8['\\'] = 'โŠค'; -utf8['\\'] = 'ยจ'; -utf8['\\'] = '๐”ฑ'; -utf8['\\'] = '๐’ฐ'; -utf8['\\'] = 'โŠด'; -utf8['\\'] = 'ยธ'; -utf8['\\'] = 'ฮบ'; -utf8['\\'] = 'โจฟ'; -utf8['\\'] = 'โ†พ'; -utf8['\\'] = 'โ‹„'; -utf8['\\'] = '๐—†'; -utf8['\\'] = '๐Ÿฒ'; -utf8['\\'] = 'โ”€'; -utf8['\\'] = 'โฆƒ'; -utf8['\\'] = 'โช…'; -utf8['\\'] = '๐”'; -utf8['\\'] = 'โ†“'; -utf8['\\'] = 'โŠ•'; -utf8['\\'] = 'โ„˜'; -utf8['\\'] = 'โˆš'; -utf8['\\'] = '๐” '; -utf8['\\'] = 'โŠฅ'; -utf8['\\'] = 'ยฉ'; -utf8['\\'] = 'โ„จ'; -utf8['\\'] = 'โˆช'; -utf8['\\'] = '๐’ฑ'; -utf8['\\'] = '๐”ฐ'; -utf8['\\'] = 'โŠต'; -utf8['\\'] = '๐–ป'; -utf8['\\'] = 'โ‡ƒ'; -utf8['\\'] = 'โ‹…'; -utf8['\\'] = '๐—‹'; -utf8['\\'] = 'โ•'; -utf8['\\'] = 'โ‡“'; -utf8['\\'] = 'โ™ข'; -utf8['\\'] = 'โŸง'; -utf8['\\'] = 'โ‰ช'; -utf8['\\'] = 'โŸท'; -utf8['\\'] = 'โ‰บ'; -utf8['\\'] = 'โˆ…'; -utf8['\\'] = 'โฆˆ'; -utf8['\\'] = 'ฮ”'; -utf8['\\'] = '๐”›'; -utf8['\\'] = 'โˆฅ'; -utf8['\\'] = '๐’ฆ'; -utf8['\\'] = '๐”ซ'; -utf8['\\'] = 'ยฎ'; -utf8['\\'] = 'โ„ณ'; -utf8['\\'] = 'ฮด'; -utf8['\\'] = 'ยพ'; -utf8['\\'] = '๐—€'; -utf8['\\'] = 'โ‰…'; -utf8['\\'] = 'ฯ„'; -utf8['\\'] = '๐—'; -utf8['\\'] = 'โ‰ฅ'; -utf8['\\'] = 'โ™ญ'; -utf8['\\'] = '๐Ÿฌ'; -utf8['\\'] = 'โจ„'; -utf8['\\'] = 'โŸผ'; -utf8['\\'] = 'โŠƒ'; -utf8['\\'] = 'โˆˆ'; -utf8['\\'] = 'โŠ“'; -utf8['\\'] = '๐”’'; -utf8['\\'] = 'โ†•'; -utf8['\\'] = 'โˆ˜'; -utf8['\\'] = 'โ„š'; -utf8['\\'] = 'โŠฃ'; -utf8['\\'] = '๐”ข'; -utf8['\\'] = 'ฮฉ'; -utf8['\\'] = 'โˆจ'; -utf8['\\'] = 'ยฏ'; -utf8['\\'] = 'โŠณ'; -utf8['\\'] = '๐”ฒ'; -utf8['\\'] = 'ฮน'; -utf8['\\'] = '๐–ฝ'; -utf8['\\'] = 'ยฟ'; -utf8['\\'] = 'โ‹ƒ'; -utf8['\\'] = 'ฯ‰'; -utf8['\\'] = 'โ‰ˆ'; -utf8['\\'] = '๐—'; -utf8['\\'] = 'โ‡•'; -utf8['\\'] = 'โ™ '; -utf8['\\'] = '๐Ÿฑ'; -utf8['\\'] = 'โˆƒ'; -utf8['\\'] = 'โŒ‰'; -utf8['\\'] = '๐”'; -utf8['\\'] = 'โˆ“'; -utf8['\\'] = 'โ„•'; -utf8['\\'] = 'โŠ˜'; -utf8['\\'] = '๐’œ'; -utf8['\\'] = 'ฮž'; -utf8['\\'] = 'ยค'; -utf8['\\'] = 'โŠจ'; -utf8['\\'] = 'โ†ช'; -utf8['\\'] = '๐”ญ'; -utf8['\\'] = '๐’ฌ'; -utf8['\\'] = 'โ„ต'; -utf8['\\'] = 'ยด'; -utf8['\\'] = 'ฮพ'; -utf8['\\'] = 'โ‰ƒ'; -utf8['\\'] = '๐—‚'; -utf8['\\'] = 'โ‹ˆ'; -utf8['\\'] = '๐—’'; -utf8['\\'] = 'โŸฆ'; -utf8['\\'] = 'โ‰ณ'; -utf8['\\'] = 'โช†'; -utf8['\\'] = 'โŸถ'; -utf8['\\'] = 'โŒˆ'; -utf8['\\'] = 'ฮ“'; -utf8['\\'] = 'โŠ™'; -utf8['\\'] = '๐”œ'; -utf8['\\'] = 'โˆž'; -utf8['\\'] = 'ฮฃ'; -utf8['\\'] = 'ยฅ'; -utf8['\\'] = 'โ„ค'; -utf8['\\'] = 'โŠฉ'; -utf8['\\'] = '๐”ฌ'; -utf8['\\'] = 'โˆฎ'; -utf8['\\'] = 'ฮณ'; -utf8['\\'] = 'โ†ฟ'; -utf8['\\'] = 'ฯƒ'; -utf8['\\'] = '๐—‡'; -utf8['\\'] = 'โฆ„'; -utf8['\\

code: 0x01d4ab group: letter -\ code: 0x01d4ac group: letter -\ code: 0x00211b group: letter -\ code: 0x01d4ae group: letter -\ code: 0x01d4af group: letter -\ code: 0x01d4b0 group: letter -\ code: 0x01d4b1 group: letter -\ code: 0x01d4b2 group: letter -\ code: 0x01d4b3 group: letter -\ code: 0x01d4b4 group: letter -\ code: 0x01d4b5 group: letter -\ code: 0x01d5ba group: letter -\ code: 0x01d5bb group: letter -\ code: 0x01d5bc group: letter -\ code: 0x01d5bd group: letter -\ code: 0x01d5be group: letter -\ code: 0x01d5bf group: letter -\ code: 0x01d5c0 group: letter -\ code: 0x01d5c1 group: letter -\ code: 0x01d5c2 group: letter -\ code: 0x01d5c3 group: letter -\ code: 0x01d5c4 group: letter -\ code: 0x01d5c5 group: letter -\ code: 0x01d5c6 group: letter -\ code: 0x01d5c7 group: letter -\ code: 0x01d5c8 group: letter -\