src/Pure/Thy/ROOT.ML
author wenzelm
Fri, 31 Oct 1997 15:21:59 +0100
changeset 4055 69892b85f800
parent 3625 33f718b4f7bf
child 4115 9405ebe284bf
permissions -rw-r--r--
Session, Context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     1
(*  Title:      Pure/Thy/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     4
                Markus Wenzel and Carsten Clasohm, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     6
This file builds the theory parser and autoloading system.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     9
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    10
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    11
use "thy_syn.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    12
3600
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    13
use "thy_info.ML";
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    14
use "browser_info.ML";
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1078
diff changeset
    15
use "thm_database.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    16
2404
edcc26b1461d added symbol_input.ML;
wenzelm
parents: 1512
diff changeset
    17
use "symbol_input.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    18
use "thy_read.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
3625
33f718b4f7bf ThmDatabase;
wenzelm
parents: 3619
diff changeset
    20
open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
1078
nipkow
parents: 431
diff changeset
    21
2809
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    22
4055
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    23
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    24
(* FIXME tmp, move *)
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    25
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    26
structure Session =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    27
struct
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    28
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    29
local
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    30
  val current_session = ref ([]: string list);
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    31
in
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    32
  fun get_session () = ! current_session;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    33
  fun add_session s =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    34
    (current_session := ! current_session @ [s];
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    35
      writeln ("This is the " ^ quote (space_implode "/" (get_session ())) ^ " session."));
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    36
end;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    37
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    38
end;
2809
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    39
4055
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    40
open Session
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    41
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    42
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    43
structure Context =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    44
struct
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    45
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    46
local
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    47
  val current_thy = ref ProtoPure.thy;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    48
in
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    49
  fun context thy = current_thy := thy;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    50
  fun get_context () = ! current_thy;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    51
end;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    52
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    53
end;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    54
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    55
open Context;