--- a/doc/Contents Sat Sep 21 12:03:51 2013 +0200
+++ b/doc/Contents Sat Sep 21 13:05:54 2013 +0200
@@ -15,6 +15,7 @@
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
+ jedit Isabelle/jEdit
Old Manuals (outdated)
intro Old Introduction to Isabelle
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/JEdit/Base.thy Sat Sep 21 13:05:54 2013 +0200
@@ -0,0 +1,8 @@
+theory Base
+imports Pure
+begin
+
+ML_file "../antiquote_setup.ML"
+setup Antiquote_Setup.setup
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/JEdit/JEdit.thy Sat Sep 21 13:05:54 2013 +0200
@@ -0,0 +1,21 @@
+theory JEdit
+imports Base
+begin
+
+chapter {* Introduction *}
+
+text {* FIXME
+
+parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP}
+
+asynchronous user interaction \cite{Wenzel:2010}, \cite{Wenzel:2012:UITP-EPTCS}
+
+document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM} \cite{Wenzel:2012}
+
+*}
+
+section {* Concepts and terminology *}
+
+text {* FIXME *}
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/JEdit/document/build Sat Sep 21 13:05:54 2013 +0200
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" logo PIDE
+
+cp "$ISABELLE_HOME/src/Doc/IsarRef/document/style.sty" .
+cp "$ISABELLE_HOME/src/Doc/iman.sty" .
+cp "$ISABELLE_HOME/src/Doc/extra.sty" .
+cp "$ISABELLE_HOME/src/Doc/isar.sty" .
+cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
+cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
+cp "$ISABELLE_HOME/src/Doc/manual.bib" .
+
+"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/JEdit/document/root.tex Sat Sep 21 13:05:54 2013 +0200
@@ -0,0 +1,41 @@
+\documentclass[12pt,a4paper]{report}
+\usepackage{supertabular}
+\usepackage{graphicx}
+\usepackage{iman,extra,isar,ttbox}
+\usepackage[nohyphen,strings]{underscore}
+\usepackage{isabelle,isabellesym}
+\usepackage{railsetup}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+
+\isadroptag{theory}
+
+\isabellestyle{literal}
+
+\title{\includegraphics[scale=0.5]{isabelle_pide} \\[4ex] Isabelle/jEdit}
+
+\author{\emph{Makarius Wenzel}}
+
+\makeindex
+
+
+\begin{document}
+
+\maketitle
+\pagenumbering{roman} \tableofcontents \clearfirst
+
+\input{JEdit.tex}
+
+\begingroup
+ \tocentry{\bibname}
+ \bibliographystyle{abbrv} \small\raggedright\frenchspacing
+ \bibliography{manual}
+\endgroup
+
+\tocentry{\indexname}
+\printindex
+
+\end{document}
--- a/src/Doc/ROOT Sat Sep 21 12:03:51 2013 +0200
+++ b/src/Doc/ROOT Sat Sep 21 13:05:54 2013 +0200
@@ -143,6 +143,23 @@
"document/showsymbols"
"document/style.sty"
+session JEdit (doc) in "JEdit" = Pure +
+ options [document_variants = "jedit", thy_output_source]
+ theories
+ JEdit
+ files
+ "../prepare_document"
+ "../IsarRef/document/style.sty"
+ "../pdfsetup.sty"
+ "../iman.sty"
+ "../extra.sty"
+ "../isar.sty"
+ "../ttbox.sty"
+ "../underscore.sty"
+ "../manual.bib"
+ "document/build"
+ "document/root.tex"
+
session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
options [document_variants = "sugar"]
theories [document = ""]
--- a/src/Doc/manual.bib Sat Sep 21 12:03:51 2013 +0200
+++ b/src/Doc/manual.bib Sat Sep 21 13:05:54 2013 +0200
@@ -1827,6 +1827,27 @@
editor = {Dos Reis, G. and L. Th\'ery},
publisher = {ACM Digital Library}}
+@InProceedings{Wenzel:2010,
+ author = {Makarius Wenzel},
+ title = {Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
+ booktitle = {User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop},
+ year = 2010,
+ editor = {C. Sacerdoti Coen and D. Aspinall},
+ series = {ENTCS},
+ month = {July},
+ publisher = {Elsevier},
+ url = {http://www.lri.fr/~wenzel/papers/async-isabelle-scala.pdf}}
+
+@InProceedings{Wenzel:2011:CICM,
+ author = {M. Wenzel},
+ title = {Isabelle as Document-oriented Proof Assistant},
+ editor = {J. H. Davenport and W. M. Farmer and F. Rabe and J. Urban},
+ booktitle = {Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)},
+ year = 2011,
+ volume = {6824},
+ series = {LNAI},
+ publisher = {Springer}}
+
@InProceedings{Wenzel:2012,
author = {Makarius Wenzel},
title = {{Isabelle/jEdit} --- a {Prover IDE} within the {PIDE} framework},
@@ -1837,6 +1858,29 @@
series = {LNAI},
publisher = {Springer}}
+@InProceedings{Wenzel:2012:UITP-EPTCS,
+ author = {Makarius Wenzel},
+ title = {{READ-EVAL-PRINT} in Parallel and Asynchronous Proof-checking},
+ booktitle = {User Interfaces for Theorem Provers (UITP 2012)},
+ year = 2013,
+ series = {EPTCS}
+}
+
+@inproceedings{Wenzel:2013:ITP,
+ author = {Makarius Wenzel},
+ title = {Shared-Memory Multiprocessing for Interactive Theorem Proving},
+ booktitle = {Interactive Theorem Proving - 4th International Conference,
+ ITP 2013, Rennes, France, July 22-26, 2013. Proceedings},
+ editor = {Sandrine Blazy and
+ Christine Paulin-Mohring and
+ David Pichardie},
+ year = {2013},
+ ee = {http://dx.doi.org/10.1007/978-3-642-39634-2_30},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ volume = {7998},
+}
+
@book{principia,
author = {A. N. Whitehead and B. Russell},
title = {Principia Mathematica},