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