src/Pure/Thy/thy_syn.ML
author paulson
Tue, 22 Jul 1997 11:14:18 +0200
changeset 3538 ed9de44032e0
parent 1512 ce37c64244c0
child 3619 0fc67ad6d62a
permissions -rw-r--r--
Removal of the tactical STATE

(*  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 -> string
  end;

functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
struct

val syntax =
  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
		       (ThyParse.pure_sections @ Data.user_sections);

val parse = ThyParse.parse_thy syntax;

end;