# HG changeset patch
# User wenzelm
# Date 1468249684 -7200
# Node ID c037248d54e89efa08edaa8643c2fcff1ad1837b
# Parent  f6b5124b7023c39d282acbbc029e9c31d7fdaed5
clarified keywords;

diff -r f6b5124b7023 -r c037248d54e8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jul 11 16:36:48 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jul 11 17:08:04 2016 +0200
@@ -163,9 +163,15 @@
   private val DOCUMENT_FILES = "document_files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
-      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
+    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+      (CHAPTER, Keyword.THY_DECL) +
+      (SESSION, Keyword.THY_DECL) +
+      (DESCRIPTION, Keyword.QUASI_COMMAND) +
+      (OPTIONS, Keyword.QUASI_COMMAND) +
+      (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
+      (THEORIES, Keyword.QUASI_COMMAND) +
+      (FILES, Keyword.QUASI_COMMAND) +
+      (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
 
   private object Parser extends Parse.Parser with Options.Parser
   {