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