basic support for session ROOT files, with examples for FOL and ZF;
authorwenzelm
Tue Jul 17 22:34:29 2012 +0200 (2012-07-17)
changeset 482807d86239986c2
parent 48279 ddf866029eb2
child 48281 6659c5913ebf
basic support for session ROOT files, with examples for FOL and ZF;
src/FOL/ROOT
src/Pure/System/build.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/modes/isabelle-session.xml
src/ZF/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOL/ROOT	Tue Jul 17 22:34:29 2012 +0200
     1.3 @@ -0,0 +1,27 @@
     1.4 +session FOL in "." = Pure +
     1.5 +  name FOL
     1.6 +  description "First-Order Logic with Natural Deduction"
     1.7 +  options [proofs = 2]
     1.8 +  theories FOL
     1.9 +  files "document/root.tex"
    1.10 +
    1.11 +session ex = FOL +
    1.12 +  theories
    1.13 +    First_Order_Logic
    1.14 +    Natural_Numbers
    1.15 +    Intro
    1.16 +    Nat
    1.17 +    Nat_Class
    1.18 +    Foundation
    1.19 +    Prolog
    1.20 +    Intuitionistic
    1.21 +    Propositional_Int
    1.22 +    Quantifiers_Int
    1.23 +    Classical
    1.24 +    Propositional_Cla
    1.25 +    Quantifiers_Cla
    1.26 +    Miniscope
    1.27 +    If
    1.28 +  theories [document = false] "Locale_Test/Locale_Test"
    1.29 +  files "document/root.tex"
    1.30 +
     2.1 --- a/src/Pure/System/build.scala	Tue Jul 17 21:49:32 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Tue Jul 17 22:34:29 2012 +0200
     2.3 @@ -56,5 +56,24 @@
     2.4  
     2.5      rc
     2.6    }
     2.7 +
     2.8 +
     2.9 +  /* session information */
    2.10 +
    2.11 +  case class Session_Info(
    2.12 +    val dir: Path,
    2.13 +    val text: String)
    2.14 +
    2.15 +  val ROOT_NAME = "ROOT"
    2.16 +
    2.17 +  def find_sessions(): List[Session_Info] =
    2.18 +  {
    2.19 +    for {
    2.20 +      dir <- Isabelle_System.components()
    2.21 +      root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
    2.22 +      if root.isFile
    2.23 +    }
    2.24 +    yield Session_Info(dir, Standard_System.read_file(root))
    2.25 +  }
    2.26  }
    2.27  
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Jul 17 21:49:32 2012 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Jul 17 22:34:29 2012 +0200
     3.3 @@ -230,7 +230,7 @@
     3.4    perl -i -e 'while (<>) {
     3.5      if (m/NAME="javacc"/) {
     3.6        print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
     3.7 -      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
     3.8 +      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
     3.9      elsif (m/NAME="scheme"/) {
    3.10        print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
    3.11      print; }' dist/modes/catalog
     4.1 --- a/src/Tools/jEdit/src/modes/isabelle-session.xml	Tue Jul 17 21:49:32 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/modes/isabelle-session.xml	Tue Jul 17 22:34:29 2012 +0200
     4.3 @@ -21,21 +21,22 @@
     4.4        <BEGIN>{*</BEGIN>
     4.5        <END>*}</END>
     4.6      </SPAN>
     4.7 -    <SPAN TYPE="LITERAL1">
     4.8 +    <SPAN TYPE="LITERAL2">
     4.9        <BEGIN>`</BEGIN>
    4.10        <END>`</END>
    4.11      </SPAN>
    4.12 -    <SPAN TYPE="LITERAL3">
    4.13 +    <SPAN TYPE="LITERAL1">
    4.14        <BEGIN>"</BEGIN>
    4.15        <END>"</END>
    4.16      </SPAN>
    4.17      <KEYWORDS>
    4.18        <KEYWORD1>session</KEYWORD1>
    4.19 -      <KEYWORD2>parent</KEYWORD2>
    4.20 -      <KEYWORD2>imports</KEYWORD2>
    4.21 -      <KEYWORD2>uses</KEYWORD2>
    4.22 +      <KEYWORD2>in</KEYWORD2>
    4.23 +      <KEYWORD2>name</KEYWORD2>
    4.24 +      <KEYWORD2>description</KEYWORD2>
    4.25 +      <KEYWORD2>files</KEYWORD2>
    4.26        <KEYWORD2>options</KEYWORD2>
    4.27 -      <KEYWORD2>dependencies</KEYWORD2>
    4.28 +      <KEYWORD2>theories</KEYWORD2>
    4.29      </KEYWORDS>
    4.30    </RULES>
    4.31  </MODE>
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/ROOT	Tue Jul 17 22:34:29 2012 +0200
     5.3 @@ -0,0 +1,148 @@
     5.4 +session ZF in "." = FOL +
     5.5 +  name ZF
     5.6 +  description {*
     5.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8 +    Copyright   1995  University of Cambridge
     5.9 +
    5.10 +    Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
    5.11 +
    5.12 +    This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
    5.13 +  *}
    5.14 +  options [document_graph]
    5.15 +  theories Main Main_ZFC
    5.16 +  files "document/root.tex"
    5.17 +
    5.18 +session AC = ZF +
    5.19 +  description {*
    5.20 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.21 +    Copyright   1995  University of Cambridge
    5.22 +
    5.23 +    Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    5.24 +  *}
    5.25 +  options [document_graph]
    5.26 +  theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6
    5.27 +    WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC
    5.28 +  files "document/root.tex" "document/root.bib"
    5.29 +
    5.30 +session Coind = ZF +
    5.31 +  description {*
    5.32 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    5.33 +    Copyright   1995  University of Cambridge
    5.34 +
    5.35 +    Coind -- A Coinduction Example.
    5.36 +
    5.37 +    Based upon the article
    5.38 +        Robin Milner and Mads Tofte,
    5.39 +        Co-induction in Relational Semantics,
    5.40 +        Theoretical Computer Science 87 (1991), pages 209-220.
    5.41 +
    5.42 +    Written up as
    5.43 +        Jacob Frost, A Case Study of Co_induction in Isabelle
    5.44 +        Report, Computer Lab, University of Cambridge (1995).
    5.45 +  *}
    5.46 +  theories ECR
    5.47 +
    5.48 +session Constructible = ZF +
    5.49 +  description {* Inner Models, Absoluteness and Consistency Proofs. *}
    5.50 +  options [document_graph]
    5.51 +  theories DPow_absolute AC_in_L Rank_Separation
    5.52 +  files "document/root.tex" "document/root.bib"
    5.53 +
    5.54 +session IMP = ZF +
    5.55 +  description {*
    5.56 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    5.57 +    Copyright   1994 TUM
    5.58 +
    5.59 +    Formalization of the denotational and operational semantics of a
    5.60 +    simple while-language, including an equivalence proof.
    5.61 +
    5.62 +    The whole development essentially formalizes/transcribes
    5.63 +    chapters 2 and 5 of
    5.64 +
    5.65 +    Glynn Winskel. The Formal Semantics of Programming Languages.
    5.66 +    MIT Press, 1993.
    5.67 +  *}
    5.68 +  theories Equiv
    5.69 +  files "document/root.tex" "document/root.bib"
    5.70 +
    5.71 +session Induct = ZF +
    5.72 +  description {*
    5.73 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.74 +    Copyright   2001  University of Cambridge
    5.75 +
    5.76 +    Inductive definitions.
    5.77 +  *}
    5.78 +  theories
    5.79 +    (** Datatypes **)
    5.80 +    Datatypes       (*sample datatypes*)
    5.81 +    Binary_Trees    (*binary trees*)
    5.82 +    Term            (*recursion over the list functor*)
    5.83 +    Ntree           (*variable-branching trees; function demo*)
    5.84 +    Tree_Forest     (*mutual recursion*)
    5.85 +    Brouwer         (*Infinite-branching trees*)
    5.86 +    Mutil           (*mutilated chess board*)
    5.87 +
    5.88 +    (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
    5.89 +    finite sets*)
    5.90 +    Multiset
    5.91 +    Rmap            (*mapping a relation over a list*)
    5.92 +    PropLog         (*completeness of propositional logic*)
    5.93 +
    5.94 +    (*two Coq examples by Christine Paulin-Mohring*)
    5.95 +    ListN
    5.96 +    Acc
    5.97 +
    5.98 +    Comb            (*Combinatory Logic example*)
    5.99 +    Primrec         (*Primitive recursive functions*)
   5.100 +  files "document/root.tex"
   5.101 +
   5.102 +session Resid = ZF +
   5.103 +  description {*
   5.104 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   5.105 +    Copyright   1995  University of Cambridge
   5.106 +
   5.107 +    Residuals -- a proof of the Church-Rosser Theorem for the
   5.108 +    untyped lambda-calculus.
   5.109 +
   5.110 +    By Ole Rasmussen, following the Coq proof given in
   5.111 +
   5.112 +    Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
   5.113 +    J. Functional Programming 4(3) 1994, 371-394.
   5.114 +  *}
   5.115 +  theories Confluence
   5.116 +
   5.117 +session UNITY = ZF +
   5.118 +  description {*
   5.119 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   5.120 +    Copyright   1998  University of Cambridge
   5.121 +
   5.122 +    ZF/UNITY proofs.
   5.123 +  *}
   5.124 +  theories
   5.125 +    (*Simple examples: no composition*)
   5.126 +    Mutex
   5.127 +
   5.128 +    (*Basic meta-theory*)
   5.129 +    Guar
   5.130 +
   5.131 +    (*Prefix relation; the Allocator example*)
   5.132 +    Distributor Merge ClientImpl AllocImpl
   5.133 +
   5.134 +session ex = ZF +
   5.135 +  description {*
   5.136 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   5.137 +    Copyright   1993  University of Cambridge
   5.138 +
   5.139 +    Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   5.140 +  *}
   5.141 +  theories
   5.142 +    misc
   5.143 +    Ring             (*abstract algebra*)
   5.144 +    Commutation      (*abstract Church-Rosser theory*)
   5.145 +    Primes           (*GCD theory*)
   5.146 +    NatSum           (*Summing integers, squares, cubes, etc.*)
   5.147 +    Ramsey           (*Simple form of Ramsey's theorem*)
   5.148 +    Limit            (*Inverse limit construction of domains*)
   5.149 +    BinEx            (*Binary integer arithmetic*)
   5.150 +    LList CoUnit     (*CoDatatypes*)
   5.151 +