# HG changeset patch
# User wenzelm
# Date 1343994951 -7200
# Node ID 730ca503e9551455d95a9ad08000eddc184ad82d
# Parent  4c7932270d6da90a480931c6cee593c77fbd632d
static outer syntax based on session specifications;

diff -r 4c7932270d6d -r 730ca503e955 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Aug 03 13:06:25 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Aug 03 13:55:51 2012 +0200
@@ -45,6 +45,12 @@
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
   val completion: Completion = Completion.empty)
 {
+  override def toString: String =
+    (for ((name, kind) <- keywords) yield {
+      if (kind == Keyword.MINOR) quote(name)
+      else quote(name) + " :: " + quote(kind)
+    }).toList.sorted.mkString("Outer_Syntax(keywords ", " and ", ")")
+
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 
   def + (name: String, kind: String, replace: String): Outer_Syntax =
diff -r 4c7932270d6d -r 730ca503e955 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Aug 03 13:06:25 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Aug 03 13:55:51 2012 +0200
@@ -264,21 +264,28 @@
 
   sealed case class Node(
     loaded_theories: Set[String],
+    syntax: Outer_Syntax,
     sources: List[(Path, SHA1.Digest)])
 
   sealed case class Deps(deps: Map[String, Node])
   {
     def is_empty: Boolean = deps.isEmpty
+    def apply(name: String): Node = deps(name)
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
   def dependencies(verbose: Boolean, queue: Session.Queue): Deps =
     Deps((Map.empty[String, Node] /: queue.topological_order)(
       { case (deps, (name, info)) =>
-          val preloaded =
+          val (preloaded, parent_syntax) =
             info.parent match {
-              case None => Set.empty[String]
-              case Some(parent) => deps(parent).loaded_theories
+              case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax)
+              case None =>
+                (Set.empty[String],
+                  Outer_Syntax.init() +
+                    // FIXME avoid hardwired stuff!?
+                    ("hence", Keyword.PRF_ASM_GOAL, "then have") +
+                    ("thus", Keyword.PRF_ASM_GOAL, "then show"))
             }
           val thy_info = new Thy_Info(new Thy_Load(preloaded))
 
@@ -296,6 +303,9 @@
 
           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
 
+          val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten
+          val syntax = (parent_syntax /: keywords)(_ + _)
+
           val all_files =
             thy_deps.map({ case (n, h) =>
               val thy = Path.explode(n.node).expand
@@ -314,7 +324,7 @@
                 error(msg + "\nThe error(s) above occurred in session " + quote(name))
             }
 
-          deps + (name -> Node(loaded_theories, sources))
+          deps + (name -> Node(loaded_theories, syntax, sources))
       }))
 
 
@@ -611,5 +621,15 @@
       }
     }
   }
+
+
+  /* static outer syntax */
+
+  // FIXME Symbol.decode!?
+  def outer_syntax(session: String): Outer_Syntax =
+  {
+    val (_, queue) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+    dependencies(false, queue)(session).syntax
+  }
 }