removed obsolete isamode.ML;
authorwenzelm
Fri Jan 11 18:07:45 2002 +0100 (2002-01-11)
changeset 127230451211bf4a0
parent 12722 5af701433ea1
child 12724 beedc794bd67
removed obsolete isamode.ML;
src/Pure/Interface/ROOT.ML
src/Pure/Interface/isamode.ML
src/Pure/IsaMakefile
src/Pure/pure.ML
     1.1 --- a/src/Pure/Interface/ROOT.ML	Fri Jan 11 18:07:30 2002 +0100
     1.2 +++ b/src/Pure/Interface/ROOT.ML	Fri Jan 11 18:07:45 2002 +0100
     1.3 @@ -4,5 +4,4 @@
     1.4  Specific support for user-interfaces.
     1.5  *)
     1.6  
     1.7 -use "isamode.ML";
     1.8  use "proof_general.ML";
     2.1 --- a/src/Pure/Interface/isamode.ML	Fri Jan 11 18:07:30 2002 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,61 +0,0 @@
     2.4 -(*  Title:      Pure/Interface/isamode.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel, TU Muenchen
     2.7 -
     2.8 -Configuration for David Aspinall's Isamode.
     2.9 -*)
    2.10 -
    2.11 -signature ISAMODE =
    2.12 -sig
    2.13 -  val setup: (theory -> theory) list
    2.14 -  val init: bool -> unit
    2.15 -end;
    2.16 -
    2.17 -structure Isamode: ISAMODE =
    2.18 -struct
    2.19 -
    2.20 -(** compile-time theory setup **)
    2.21 -
    2.22 -(* token translations *)
    2.23 -
    2.24 -val isamodeN = "Isamode";
    2.25 -
    2.26 -local
    2.27 -
    2.28 -val end_tag = "\^A0";
    2.29 -val tclass_tag = "\^A1";
    2.30 -val tfree_tag = "\^A2";
    2.31 -val tvar_tag = "\^A3";
    2.32 -val free_tag = "\^A4";
    2.33 -val bound_tag = "\^A5";
    2.34 -val var_tag = "\^A6";
    2.35 -
    2.36 -fun tagit p x = (p ^ x ^ end_tag, real (size x));
    2.37 -
    2.38 -in
    2.39 -
    2.40 -val isamode_trans =
    2.41 - Syntax.tokentrans_mode isamodeN
    2.42 -  [("class", tagit tclass_tag),
    2.43 -   ("tfree", tagit tfree_tag),
    2.44 -   ("tvar", tagit tvar_tag),
    2.45 -   ("free", tagit free_tag),
    2.46 -   ("bound", tagit bound_tag),
    2.47 -   ("var", tagit var_tag)];
    2.48 -
    2.49 -end;
    2.50 -
    2.51 -
    2.52 -(* setup *)
    2.53 -
    2.54 -val setup = [Theory.add_tokentrfuns isamode_trans];
    2.55 -
    2.56 -
    2.57 -
    2.58 -(** run-time initialization **)
    2.59 -
    2.60 -fun init isamode =
    2.61 -  if isamode then print_mode := isamodeN :: ! print_mode else ();
    2.62 -
    2.63 -
    2.64 -end;
     3.1 --- a/src/Pure/IsaMakefile	Fri Jan 11 18:07:30 2002 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Fri Jan 11 18:07:45 2002 +0100
     3.3 @@ -28,11 +28,11 @@
     3.4    General/name_space.ML General/object.ML General/path.ML		\
     3.5    General/position.ML General/pretty.ML General/scan.ML General/seq.ML	\
     3.6    General/source.ML General/symbol.ML General/table.ML General/url.ML	\
     3.7 -  General/xml.ML Interface/ROOT.ML Interface/isamode.ML			\
     3.8 -  Interface/proof_general.ML Isar/ROOT.ML Isar/antiquote.ML 		\
     3.9 -  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
    3.10 -  Isar/comment.ML Isar/context_rules.ML Isar/induct_attrib.ML 		\
    3.11 -  Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML	\
    3.12 +  General/xml.ML Interface/ROOT.ML Interface/proof_general.ML		\
    3.13 +  Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
    3.14 +  Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML			\
    3.15 +  Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
    3.16 +  Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML			\
    3.17    Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
    3.18    Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML			\
    3.19    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML		\
     4.1 --- a/src/Pure/pure.ML	Fri Jan 11 18:07:30 2002 +0100
     4.2 +++ b/src/Pure/pure.ML	Fri Jan 11 18:07:45 2002 +0100
     4.3 @@ -21,7 +21,6 @@
     4.4      AxClass.setup @
     4.5      Latex.setup @
     4.6      Present.setup @
     4.7 -    Isamode.setup @
     4.8      ProofGeneral.setup @
     4.9      Codegen.setup @
    4.10      Goals.setup;