# HG changeset patch
# User wenzelm
# Date 770478296 -7200
# Node ID 4860901706db2ab29ff8560117019fd79cccd714
# Parent  c8171ee32744bdce6514047bbfdbc168827c2ae2
interface for 'user sections';

diff -r c8171ee32744 -r 4860901706db src/Pure/Thy/thy_syn.ML
--- /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;
+