src/Pure/Thy/thy_syn.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 476 836cad329311
child 3619 0fc67ad6d62a
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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