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