src/Pure/Thy/thy_syn.ML
author wenzelm
Wed Oct 17 18:52:30 2001 +0200 (2001-10-17)
changeset 11819 9283b3c11234
parent 7024 44bd3c094fd6
child 12120 a08c61932501
permissions -rw-r--r--
tuned comments;
     1 (*  Title:      Pure/Thy/thy_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Provide syntax for *old-style* theory files.
     7 *)
     8 
     9 signature BASIC_THY_SYN =
    10 sig
    11   val delete_tmpfiles: bool ref
    12 end;
    13 
    14 signature THY_SYN =
    15 sig
    16   include BASIC_THY_SYN
    17   val add_syntax: string list ->
    18     (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
    19     -> unit
    20   val get_lexicon: unit -> Scan.lexicon
    21   val load_thy: string -> string list -> unit
    22 end;
    23 
    24 structure ThySyn: THY_SYN =
    25 struct
    26 
    27 
    28 (* current syntax *)
    29 
    30 val keywords = ref ThyParse.pure_keywords;
    31 val sections = ref ThyParse.pure_sections;
    32 
    33 fun make_syntax () =
    34   ThyParse.make_syntax (! keywords) (!sections);
    35 
    36 val syntax = ref (make_syntax ());
    37 
    38 fun get_lexicon () = ThyParse.get_lexicon (! syntax);
    39 
    40 
    41 (* augment syntax *)
    42 
    43 fun add_syntax keys sects =
    44  (keywords := (keys union ! keywords);
    45   sections := sects @ ! sections;
    46   syntax := make_syntax ());
    47 
    48 
    49 (* load_thy *)
    50 
    51 val delete_tmpfiles = ref true;
    52 
    53 fun load_thy name chs =
    54   let
    55     val tmp_path = File.tmp_path (ThyLoad.ml_path (name ^ "_thy"));
    56     val txt_out = ThyParse.parse_thy (! syntax) chs;
    57   in
    58     File.write tmp_path txt_out;
    59     File.symbol_use tmp_path;
    60     if ! delete_tmpfiles then File.rm tmp_path else ()
    61   end;
    62 
    63 
    64 end;
    65 
    66 
    67 structure BasicThySyn: BASIC_THY_SYN = ThySyn;
    68 open BasicThySyn;