interface for 'user sections';

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_syn.ML	Wed Jun 01 15:44:56 1994 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Pure/Thy/thy_syn.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Interface for user syntax.
+*)
+
+signature THY_SYN_DATA =
+sig
+  val user_keywords: string list
+  val user_sections: (string * (ThyParse.token list -> (string * string)
+    * ThyParse.token list)) list
+end;
+
+signature THY_SYN =
+sig
+  val parse: string -> string
+end;
+
+functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
+struct
+
+open ThyParse ThySynData;
+
+val syntax =
+  make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
+
+val parse = parse_thy syntax;
+
+end;
+