# HG changeset patch
# User wenzelm
# Date 1342557269 -7200
# Node ID 7d86239986c21c12076e547133a789fd5fab7b3a
# Parent  ddf866029eb28481992f0930307805c9d0a45e51
basic support for session ROOT files, with examples for FOL and ZF;

diff -r ddf866029eb2 -r 7d86239986c2 src/FOL/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ROOT	Tue Jul 17 22:34:29 2012 +0200
@@ -0,0 +1,27 @@
+session FOL in "." = Pure +
+  name FOL
+  description "First-Order Logic with Natural Deduction"
+  options [proofs = 2]
+  theories FOL
+  files "document/root.tex"
+
+session ex = FOL +
+  theories
+    First_Order_Logic
+    Natural_Numbers
+    Intro
+    Nat
+    Nat_Class
+    Foundation
+    Prolog
+    Intuitionistic
+    Propositional_Int
+    Quantifiers_Int
+    Classical
+    Propositional_Cla
+    Quantifiers_Cla
+    Miniscope
+    If
+  theories [document = false] "Locale_Test/Locale_Test"
+  files "document/root.tex"
+
diff -r ddf866029eb2 -r 7d86239986c2 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 17 22:34:29 2012 +0200
@@ -56,5 +56,24 @@
 
     rc
   }
+
+
+  /* session information */
+
+  case class Session_Info(
+    val dir: Path,
+    val text: String)
+
+  val ROOT_NAME = "ROOT"
+
+  def find_sessions(): List[Session_Info] =
+  {
+    for {
+      dir <- Isabelle_System.components()
+      root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
+      if root.isFile
+    }
+    yield Session_Info(dir, Standard_System.read_file(root))
+  }
 }
 
diff -r ddf866029eb2 -r 7d86239986c2 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Jul 17 22:34:29 2012 +0200
@@ -230,7 +230,7 @@
   perl -i -e 'while (<>) {
     if (m/NAME="javacc"/) {
       print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
-      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
+      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
     elsif (m/NAME="scheme"/) {
       print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
     print; }' dist/modes/catalog
diff -r ddf866029eb2 -r 7d86239986c2 src/Tools/jEdit/src/modes/isabelle-session.xml
--- a/src/Tools/jEdit/src/modes/isabelle-session.xml	Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-session.xml	Tue Jul 17 22:34:29 2012 +0200
@@ -21,21 +21,22 @@
       <BEGIN>{*</BEGIN>
       <END>*}</END>
     </SPAN>
-    <SPAN TYPE="LITERAL1">
+    <SPAN TYPE="LITERAL2">
       <BEGIN>`</BEGIN>
       <END>`</END>
     </SPAN>
-    <SPAN TYPE="LITERAL3">
+    <SPAN TYPE="LITERAL1">
       <BEGIN>"</BEGIN>
       <END>"</END>
     </SPAN>
     <KEYWORDS>
       <KEYWORD1>session</KEYWORD1>
-      <KEYWORD2>parent</KEYWORD2>
-      <KEYWORD2>imports</KEYWORD2>
-      <KEYWORD2>uses</KEYWORD2>
+      <KEYWORD2>in</KEYWORD2>
+      <KEYWORD2>name</KEYWORD2>
+      <KEYWORD2>description</KEYWORD2>
+      <KEYWORD2>files</KEYWORD2>
       <KEYWORD2>options</KEYWORD2>
-      <KEYWORD2>dependencies</KEYWORD2>
+      <KEYWORD2>theories</KEYWORD2>
     </KEYWORDS>
   </RULES>
 </MODE>
diff -r ddf866029eb2 -r 7d86239986c2 src/ZF/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ROOT	Tue Jul 17 22:34:29 2012 +0200
@@ -0,0 +1,148 @@
+session ZF in "." = FOL +
+  name ZF
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+    Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+
+    This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+  *}
+  options [document_graph]
+  theories Main Main_ZFC
+  files "document/root.tex"
+
+session AC = ZF +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+    Proofs of AC-equivalences, due to Krzysztof Grabczewski.
+  *}
+  options [document_graph]
+  theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6
+    WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC
+  files "document/root.tex" "document/root.bib"
+
+session Coind = ZF +
+  description {*
+    Author:     Jacob Frost, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+    Coind -- A Coinduction Example.
+
+    Based upon the article
+        Robin Milner and Mads Tofte,
+        Co-induction in Relational Semantics,
+        Theoretical Computer Science 87 (1991), pages 209-220.
+
+    Written up as
+        Jacob Frost, A Case Study of Co_induction in Isabelle
+        Report, Computer Lab, University of Cambridge (1995).
+  *}
+  theories ECR
+
+session Constructible = ZF +
+  description {* Inner Models, Absoluteness and Consistency Proofs. *}
+  options [document_graph]
+  theories DPow_absolute AC_in_L Rank_Separation
+  files "document/root.tex" "document/root.bib"
+
+session IMP = ZF +
+  description {*
+    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+
+    Formalization of the denotational and operational semantics of a
+    simple while-language, including an equivalence proof.
+
+    The whole development essentially formalizes/transcribes
+    chapters 2 and 5 of
+
+    Glynn Winskel. The Formal Semantics of Programming Languages.
+    MIT Press, 1993.
+  *}
+  theories Equiv
+  files "document/root.tex" "document/root.bib"
+
+session Induct = ZF +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+
+    Inductive definitions.
+  *}
+  theories
+    (** Datatypes **)
+    Datatypes       (*sample datatypes*)
+    Binary_Trees    (*binary trees*)
+    Term            (*recursion over the list functor*)
+    Ntree           (*variable-branching trees; function demo*)
+    Tree_Forest     (*mutual recursion*)
+    Brouwer         (*Infinite-branching trees*)
+    Mutil           (*mutilated chess board*)
+
+    (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
+    finite sets*)
+    Multiset
+    Rmap            (*mapping a relation over a list*)
+    PropLog         (*completeness of propositional logic*)
+
+    (*two Coq examples by Christine Paulin-Mohring*)
+    ListN
+    Acc
+
+    Comb            (*Combinatory Logic example*)
+    Primrec         (*Primitive recursive functions*)
+  files "document/root.tex"
+
+session Resid = ZF +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+    Residuals -- a proof of the Church-Rosser Theorem for the
+    untyped lambda-calculus.
+
+    By Ole Rasmussen, following the Coq proof given in
+
+    Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
+    J. Functional Programming 4(3) 1994, 371-394.
+  *}
+  theories Confluence
+
+session UNITY = ZF +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+    ZF/UNITY proofs.
+  *}
+  theories
+    (*Simple examples: no composition*)
+    Mutex
+
+    (*Basic meta-theory*)
+    Guar
+
+    (*Prefix relation; the Allocator example*)
+    Distributor Merge ClientImpl AllocImpl
+
+session ex = ZF +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+    Miscellaneous examples for Zermelo-Fraenkel Set Theory.
+  *}
+  theories
+    misc
+    Ring             (*abstract algebra*)
+    Commutation      (*abstract Church-Rosser theory*)
+    Primes           (*GCD theory*)
+    NatSum           (*Summing integers, squares, cubes, etc.*)
+    Ramsey           (*Simple form of Ramsey's theorem*)
+    Limit            (*Inverse limit construction of domains*)
+    BinEx            (*Binary integer arithmetic*)
+    LList CoUnit     (*CoDatatypes*)
+