basic setup for Isabelle/jEdit documentation;
authorwenzelm
Sat Sep 21 13:05:54 2013 +0200 (2013-09-21)
changeset 53769036e80175bdd
parent 53768 46a2154f250c
child 53770 db362319d766
basic setup for Isabelle/jEdit documentation;
doc/Contents
src/Doc/JEdit/Base.thy
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/build
src/Doc/JEdit/document/root.tex
src/Doc/ROOT
src/Doc/manual.bib
     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},