# HG changeset patch # User wenzelm # Date 1379761554 -7200 # Node ID 036e80175bddff312602b3edb18ac5930a51aea5 # Parent 46a2154f250c9f8b3acebcf1b9ca60ab8e10bfcc basic setup for Isabelle/jEdit documentation; diff -r 46a2154f250c -r 036e80175bdd doc/Contents --- 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 diff -r 46a2154f250c -r 036e80175bdd src/Doc/JEdit/Base.thy --- /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 diff -r 46a2154f250c -r 036e80175bdd src/Doc/JEdit/JEdit.thy --- /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 diff -r 46a2154f250c -r 036e80175bdd src/Doc/JEdit/document/build --- /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" + diff -r 46a2154f250c -r 036e80175bdd src/Doc/JEdit/document/root.tex --- /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} diff -r 46a2154f250c -r 036e80175bdd src/Doc/ROOT --- 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 = ""] diff -r 46a2154f250c -r 036e80175bdd src/Doc/manual.bib --- 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},