src/Pure/Thy/thy_syn.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 476 836cad329311
child 1512 ce37c64244c0
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
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 =
wenzelm@411
     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
wenzelm@411
    13
end;
wenzelm@411
    14
wenzelm@411
    15
signature THY_SYN =
wenzelm@411
    16
sig
clasohm@476
    17
  val parse: string -> string -> string
wenzelm@411
    18
end;
wenzelm@411
    19
wenzelm@411
    20
functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
wenzelm@411
    21
struct
wenzelm@411
    22
wenzelm@411
    23
open ThyParse ThySynData;
wenzelm@411
    24
wenzelm@411
    25
val syntax =
wenzelm@411
    26
  make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
wenzelm@411
    27
wenzelm@411
    28
val parse = parse_thy syntax;
wenzelm@411
    29
wenzelm@411
    30
end;
wenzelm@411
    31