1.1 --- a/doc/Contents Sat Sep 21 12:03:51 2013 +0200
1.2 +++ b/doc/Contents Sat Sep 21 13:05:54 2013 +0200
1.3 @@ -15,6 +15,7 @@
1.4 isar-ref The Isabelle/Isar Reference Manual
1.5 implementation The Isabelle/Isar Implementation Manual
1.6 system The Isabelle System Manual
1.7 + jedit Isabelle/jEdit
1.8
1.9 Old Manuals (outdated)
1.10 intro Old Introduction to Isabelle
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Doc/JEdit/Base.thy Sat Sep 21 13:05:54 2013 +0200
2.3 @@ -0,0 +1,8 @@
2.4 +theory Base
2.5 +imports Pure
2.6 +begin
2.7 +
2.8 +ML_file "../antiquote_setup.ML"
2.9 +setup Antiquote_Setup.setup
2.10 +
2.11 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Doc/JEdit/JEdit.thy Sat Sep 21 13:05:54 2013 +0200
3.3 @@ -0,0 +1,21 @@
3.4 +theory JEdit
3.5 +imports Base
3.6 +begin
3.7 +
3.8 +chapter {* Introduction *}
3.9 +
3.10 +text {* FIXME
3.11 +
3.12 +parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP}
3.13 +
3.14 +asynchronous user interaction \cite{Wenzel:2010}, \cite{Wenzel:2012:UITP-EPTCS}
3.15 +
3.16 +document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM} \cite{Wenzel:2012}
3.17 +
3.18 +*}
3.19 +
3.20 +section {* Concepts and terminology *}
3.21 +
3.22 +text {* FIXME *}
3.23 +
3.24 +end
3.25 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Doc/JEdit/document/build Sat Sep 21 13:05:54 2013 +0200
4.3 @@ -0,0 +1,19 @@
4.4 +#!/usr/bin/env bash
4.5 +
4.6 +set -e
4.7 +
4.8 +FORMAT="$1"
4.9 +VARIANT="$2"
4.10 +
4.11 +"$ISABELLE_TOOL" logo PIDE
4.12 +
4.13 +cp "$ISABELLE_HOME/src/Doc/IsarRef/document/style.sty" .
4.14 +cp "$ISABELLE_HOME/src/Doc/iman.sty" .
4.15 +cp "$ISABELLE_HOME/src/Doc/extra.sty" .
4.16 +cp "$ISABELLE_HOME/src/Doc/isar.sty" .
4.17 +cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
4.18 +cp "$ISABELLE_HOME/src/Doc/underscore.sty" .
4.19 +cp "$ISABELLE_HOME/src/Doc/manual.bib" .
4.20 +
4.21 +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
4.22 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Doc/JEdit/document/root.tex Sat Sep 21 13:05:54 2013 +0200
5.3 @@ -0,0 +1,41 @@
5.4 +\documentclass[12pt,a4paper]{report}
5.5 +\usepackage{supertabular}
5.6 +\usepackage{graphicx}
5.7 +\usepackage{iman,extra,isar,ttbox}
5.8 +\usepackage[nohyphen,strings]{underscore}
5.9 +\usepackage{isabelle,isabellesym}
5.10 +\usepackage{railsetup}
5.11 +\usepackage{style}
5.12 +\usepackage{pdfsetup}
5.13 +
5.14 +\hyphenation{Isabelle}
5.15 +\hyphenation{Isar}
5.16 +
5.17 +\isadroptag{theory}
5.18 +
5.19 +\isabellestyle{literal}
5.20 +
5.21 +\title{\includegraphics[scale=0.5]{isabelle_pide} \\[4ex] Isabelle/jEdit}
5.22 +
5.23 +\author{\emph{Makarius Wenzel}}
5.24 +
5.25 +\makeindex
5.26 +
5.27 +
5.28 +\begin{document}
5.29 +
5.30 +\maketitle
5.31 +\pagenumbering{roman} \tableofcontents \clearfirst
5.32 +
5.33 +\input{JEdit.tex}
5.34 +
5.35 +\begingroup
5.36 + \tocentry{\bibname}
5.37 + \bibliographystyle{abbrv} \small\raggedright\frenchspacing
5.38 + \bibliography{manual}
5.39 +\endgroup
5.40 +
5.41 +\tocentry{\indexname}
5.42 +\printindex
5.43 +
5.44 +\end{document}
6.1 --- a/src/Doc/ROOT Sat Sep 21 12:03:51 2013 +0200
6.2 +++ b/src/Doc/ROOT Sat Sep 21 13:05:54 2013 +0200
6.3 @@ -143,6 +143,23 @@
6.4 "document/showsymbols"
6.5 "document/style.sty"
6.6
6.7 +session JEdit (doc) in "JEdit" = Pure +
6.8 + options [document_variants = "jedit", thy_output_source]
6.9 + theories
6.10 + JEdit
6.11 + files
6.12 + "../prepare_document"
6.13 + "../IsarRef/document/style.sty"
6.14 + "../pdfsetup.sty"
6.15 + "../iman.sty"
6.16 + "../extra.sty"
6.17 + "../isar.sty"
6.18 + "../ttbox.sty"
6.19 + "../underscore.sty"
6.20 + "../manual.bib"
6.21 + "document/build"
6.22 + "document/root.tex"
6.23 +
6.24 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
6.25 options [document_variants = "sugar"]
6.26 theories [document = ""]
7.1 --- a/src/Doc/manual.bib Sat Sep 21 12:03:51 2013 +0200
7.2 +++ b/src/Doc/manual.bib Sat Sep 21 13:05:54 2013 +0200
7.3 @@ -1827,6 +1827,27 @@
7.4 editor = {Dos Reis, G. and L. Th\'ery},
7.5 publisher = {ACM Digital Library}}
7.6
7.7 +@InProceedings{Wenzel:2010,
7.8 + author = {Makarius Wenzel},
7.9 + title = {Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
7.10 + booktitle = {User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop},
7.11 + year = 2010,
7.12 + editor = {C. Sacerdoti Coen and D. Aspinall},
7.13 + series = {ENTCS},
7.14 + month = {July},
7.15 + publisher = {Elsevier},
7.16 + url = {http://www.lri.fr/~wenzel/papers/async-isabelle-scala.pdf}}
7.17 +
7.18 +@InProceedings{Wenzel:2011:CICM,
7.19 + author = {M. Wenzel},
7.20 + title = {Isabelle as Document-oriented Proof Assistant},
7.21 + editor = {J. H. Davenport and W. M. Farmer and F. Rabe and J. Urban},
7.22 + booktitle = {Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)},
7.23 + year = 2011,
7.24 + volume = {6824},
7.25 + series = {LNAI},
7.26 + publisher = {Springer}}
7.27 +
7.28 @InProceedings{Wenzel:2012,
7.29 author = {Makarius Wenzel},
7.30 title = {{Isabelle/jEdit} --- a {Prover IDE} within the {PIDE} framework},
7.31 @@ -1837,6 +1858,29 @@
7.32 series = {LNAI},
7.33 publisher = {Springer}}
7.34
7.35 +@InProceedings{Wenzel:2012:UITP-EPTCS,
7.36 + author = {Makarius Wenzel},
7.37 + title = {{READ-EVAL-PRINT} in Parallel and Asynchronous Proof-checking},
7.38 + booktitle = {User Interfaces for Theorem Provers (UITP 2012)},
7.39 + year = 2013,
7.40 + series = {EPTCS}
7.41 +}
7.42 +
7.43 +@inproceedings{Wenzel:2013:ITP,
7.44 + author = {Makarius Wenzel},
7.45 + title = {Shared-Memory Multiprocessing for Interactive Theorem Proving},
7.46 + booktitle = {Interactive Theorem Proving - 4th International Conference,
7.47 + ITP 2013, Rennes, France, July 22-26, 2013. Proceedings},
7.48 + editor = {Sandrine Blazy and
7.49 + Christine Paulin-Mohring and
7.50 + David Pichardie},
7.51 + year = {2013},
7.52 + ee = {http://dx.doi.org/10.1007/978-3-642-39634-2_30},
7.53 + publisher = {Springer},
7.54 + series = {Lecture Notes in Computer Science},
7.55 + volume = {7998},
7.56 +}
7.57 +
7.58 @book{principia,
7.59 author = {A. N. Whitehead and B. Russell},
7.60 title = {Principia Mathematica},