src/Pure/Thy/ROOT.ML
author wenzelm
Tue, 04 Nov 1997 12:46:50 +0100
changeset 4115 9405ebe284bf
parent 4055 69892b85f800
child 4214 523f6bea9fd7
permissions -rw-r--r--
added path.ML;
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
4115
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
     9
use "path.ML";
9405ebe284bf added path.ML;
wenzelm
parents: 4055
diff changeset
    10
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    11
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    12
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    13
use "thy_syn.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    14
3600
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    15
use "thy_info.ML";
5366dde08dba Added some additional "use" commands for new files
berghofe
parents: 3576
diff changeset
    16
use "browser_info.ML";
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1078
diff changeset
    17
use "thm_database.ML";
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3600
diff changeset
    18
2404
edcc26b1461d added symbol_input.ML;
wenzelm
parents: 1512
diff changeset
    19
use "symbol_input.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    20
use "thy_read.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
3625
33f718b4f7bf ThmDatabase;
wenzelm
parents: 3619
diff changeset
    22
open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
1078
nipkow
parents: 431
diff changeset
    23
2809
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    24
4055
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    25
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    26
(* FIXME tmp, move *)
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    27
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    28
structure Session =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    29
struct
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    30
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    31
local
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    32
  val current_session = ref ([]: string list);
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    33
in
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    34
  fun get_session () = ! current_session;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    35
  fun add_session s =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    36
    (current_session := ! current_session @ [s];
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    37
      writeln ("This is the " ^ quote (space_implode "/" (get_session ())) ^ " session."));
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    38
end;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    39
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    40
end;
2809
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    41
4055
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    42
open Session
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    43
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    44
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    45
structure Context =
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    46
struct
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    47
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    48
local
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    49
  val current_thy = ref ProtoPure.thy;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    50
in
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    51
  fun context thy = current_thy := thy;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    52
  fun get_context () = ! current_thy;
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
end;
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    56
69892b85f800 Session, Context;
wenzelm
parents: 3625
diff changeset
    57
open Context;