--- a/src/Pure/Interface/ROOT.ML Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/Interface/ROOT.ML Fri Jan 11 18:07:45 2002 +0100
@@ -4,5 +4,4 @@
Specific support for user-interfaces.
*)
-use "isamode.ML";
use "proof_general.ML";
--- a/src/Pure/Interface/isamode.ML Fri Jan 11 18:07:30 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Title: Pure/Interface/isamode.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Configuration for David Aspinall's Isamode.
-*)
-
-signature ISAMODE =
-sig
- val setup: (theory -> theory) list
- val init: bool -> unit
-end;
-
-structure Isamode: ISAMODE =
-struct
-
-(** compile-time theory setup **)
-
-(* token translations *)
-
-val isamodeN = "Isamode";
-
-local
-
-val end_tag = "\^A0";
-val tclass_tag = "\^A1";
-val tfree_tag = "\^A2";
-val tvar_tag = "\^A3";
-val free_tag = "\^A4";
-val bound_tag = "\^A5";
-val var_tag = "\^A6";
-
-fun tagit p x = (p ^ x ^ end_tag, real (size x));
-
-in
-
-val isamode_trans =
- Syntax.tokentrans_mode isamodeN
- [("class", tagit tclass_tag),
- ("tfree", tagit tfree_tag),
- ("tvar", tagit tvar_tag),
- ("free", tagit free_tag),
- ("bound", tagit bound_tag),
- ("var", tagit var_tag)];
-
-end;
-
-
-(* setup *)
-
-val setup = [Theory.add_tokentrfuns isamode_trans];
-
-
-
-(** run-time initialization **)
-
-fun init isamode =
- if isamode then print_mode := isamodeN :: ! print_mode else ();
-
-
-end;
--- a/src/Pure/IsaMakefile Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/IsaMakefile Fri Jan 11 18:07:45 2002 +0100
@@ -28,11 +28,11 @@
General/name_space.ML General/object.ML General/path.ML \
General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
General/source.ML General/symbol.ML General/table.ML General/url.ML \
- General/xml.ML Interface/ROOT.ML Interface/isamode.ML \
- Interface/proof_general.ML Isar/ROOT.ML Isar/antiquote.ML \
- Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
- Isar/comment.ML Isar/context_rules.ML Isar/induct_attrib.ML \
- Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML \
+ General/xml.ML Interface/ROOT.ML Interface/proof_general.ML \
+ Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
+ Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML \
+ Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \
+ Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML \
Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \
Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
--- a/src/Pure/pure.ML Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/pure.ML Fri Jan 11 18:07:45 2002 +0100
@@ -21,7 +21,6 @@
AxClass.setup @
Latex.setup @
Present.setup @
- Isamode.setup @
ProofGeneral.setup @
Codegen.setup @
Goals.setup;