src/Pure/Thy/thy_syn.ML
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 1512 ce37c64244c0
child 3619 0fc67ad6d62a
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
     1 (*  Title:      Pure/Thy/thy_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Interface for user syntax.
     6 *)
     7 
     8 signature THY_SYN_DATA =
     9   sig
    10   val user_keywords: string list
    11   val user_sections: (string * (ThyParse.token list -> (string * string)
    12     * ThyParse.token list)) list
    13   end;
    14 
    15 signature THY_SYN =
    16   sig
    17   val parse: string -> string -> string
    18   end;
    19 
    20 functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
    21 struct
    22 
    23 val syntax =
    24   ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
    25 		       (ThyParse.pure_sections @ Data.user_sections);
    26 
    27 val parse = ThyParse.parse_thy syntax;
    28 
    29 end;
    30