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);
wenzelm@411
     1
(*  Title:      Pure/Thy/thy_syn.ML
wenzelm@411
     2
    ID:         $Id$
wenzelm@411
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@411
     4
wenzelm@411
     5
Interface for user syntax.
wenzelm@411
     6
*)
wenzelm@411
     7
wenzelm@411
     8
signature THY_SYN_DATA =
paulson@1512
     9
  sig
wenzelm@411
    10
  val user_keywords: string list
wenzelm@411
    11
  val user_sections: (string * (ThyParse.token list -> (string * string)
wenzelm@411
    12
    * ThyParse.token list)) list
paulson@1512
    13
  end;
wenzelm@411
    14
wenzelm@411
    15
signature THY_SYN =
paulson@1512
    16
  sig
clasohm@476
    17
  val parse: string -> string -> string
paulson@1512
    18
  end;
wenzelm@411
    19
paulson@1512
    20
functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
wenzelm@411
    21
struct
wenzelm@411
    22
paulson@1512
    23
val syntax =
paulson@1512
    24
  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
paulson@1512
    25
		       (ThyParse.pure_sections @ Data.user_sections);
wenzelm@411
    26
paulson@1512
    27
val parse = ThyParse.parse_thy syntax;
wenzelm@411
    28
wenzelm@411
    29
end;
wenzelm@411
    30