removed unused properties;
authorwenzelm
Thu Jan 24 23:51:22 2008 +0100 (2008-01-24)
changeset 259601f9956e0bd89
parent 25959 9ad285dbc7a4
child 25961 ec39d7e40554
removed unused properties;
replaced ContextPosition by Position.thread_data;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 24 23:51:20 2008 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 24 23:51:22 2008 +0100
     1.3 @@ -46,10 +46,8 @@
     1.4    val undo_limit: bool -> int option
     1.5    val empty: transition
     1.6    val name_of: transition -> string
     1.7 -  val properties_of: transition -> Markup.property list
     1.8    val source_of: transition -> OuterLex.token list option
     1.9    val name: string -> transition -> transition
    1.10 -  val properties: Markup.property list -> transition -> transition
    1.11    val position: Position.T -> transition -> transition
    1.12    val source: OuterLex.token list -> transition -> transition
    1.13    val interactive: bool -> transition -> transition
    1.14 @@ -343,12 +341,6 @@
    1.15    (fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE)
    1.16      | node => node);
    1.17  
    1.18 -fun context_position pos = History.map_current
    1.19 -  (fn Theory (gthy, ctxt) => Theory (ContextPosition.put pos gthy, ctxt)
    1.20 -    | Proof (prf, x) =>
    1.21 -        Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put_ctxt pos)) prf, x)
    1.22 -    | node => node);
    1.23 -
    1.24  fun return (result, NONE) = result
    1.25    | return (result, SOME exn) = raise FAILURE (result, exn);
    1.26  
    1.27 @@ -364,12 +356,9 @@
    1.28  
    1.29      val (result, err) =
    1.30        cont_node
    1.31 -      |> context_position pos
    1.32 -      |> map_theory Theory.checkpoint
    1.33        |> (f
    1.34            |> (if hist then History.apply' (History.current back_node) else History.map_current)
    1.35            |> controlled_execution)
    1.36 -      |> context_position Position.none
    1.37        |> normal_state
    1.38        handle exn => error_state cont_node exn;
    1.39    in
    1.40 @@ -448,7 +437,6 @@
    1.41  
    1.42  datatype transition = Transition of
    1.43   {name: string,                        (*command name*)
    1.44 -  props: Markup.property list,         (*properties*)
    1.45    pos: Position.T,                     (*source position*)
    1.46    source: OuterLex.token list option,  (*source text*)
    1.47    int_only: bool,                      (*interactive-only*)
    1.48 @@ -456,17 +444,16 @@
    1.49    no_timing: bool,                     (*suppress timing*)
    1.50    trans: trans list};                  (*primitive transitions (union)*)
    1.51  
    1.52 -fun make_transition (name, props, pos, source, int_only, print, no_timing, trans) =
    1.53 -  Transition {name = name, props = props, pos = pos, source = source,
    1.54 +fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
    1.55 +  Transition {name = name, pos = pos, source = source,
    1.56      int_only = int_only, print = print, no_timing = no_timing, trans = trans};
    1.57  
    1.58 -fun map_transition f (Transition {name, props, pos, source, int_only, print, no_timing, trans}) =
    1.59 -  make_transition (f (name, props, pos, source, int_only, print, no_timing, trans));
    1.60 +fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
    1.61 +  make_transition (f (name, pos, source, int_only, print, no_timing, trans));
    1.62  
    1.63 -val empty = make_transition ("<unknown>", [], Position.none, NONE, false, [], false, []);
    1.64 +val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
    1.65  
    1.66  fun name_of (Transition {name, ...}) = name;
    1.67 -fun properties_of (Transition {props, ...}) = props;
    1.68  fun source_of (Transition {source, ...}) = source;
    1.69  
    1.70  
    1.71 @@ -483,37 +470,26 @@
    1.72  
    1.73  (* modify transitions *)
    1.74  
    1.75 -fun name nm =
    1.76 -  map_transition (fn (_, props, pos, source, int_only, print, no_timing, trans) =>
    1.77 -    (nm, props, pos, source, int_only, print, no_timing, trans));
    1.78 -
    1.79 -fun properties props =
    1.80 -  map_transition (fn (name, _, pos, source, int_only, print, no_timing, trans) =>
    1.81 -    (name, props, pos, source, int_only, print, no_timing, trans));
    1.82 +fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
    1.83 +  (nm, pos, source, int_only, print, no_timing, trans));
    1.84  
    1.85 -fun position pos =
    1.86 -  map_transition (fn (name, props, _, source, int_only, print, no_timing, trans) =>
    1.87 -    (name, props, pos, source, int_only, print, no_timing, trans));
    1.88 +fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
    1.89 +  (name, pos, source, int_only, print, no_timing, trans));
    1.90  
    1.91 -fun source src =
    1.92 -  map_transition (fn (name, props, pos, _, int_only, print, no_timing, trans) =>
    1.93 -    (name, props, pos, SOME src, int_only, print, no_timing, trans));
    1.94 +fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
    1.95 +  (name, pos, SOME src, int_only, print, no_timing, trans));
    1.96  
    1.97 -fun interactive int_only =
    1.98 -  map_transition (fn (name, props, pos, source, _, print, no_timing, trans) =>
    1.99 -    (name, props, pos, source, int_only, print, no_timing, trans));
   1.100 +fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
   1.101 +  (name, pos, source, int_only, print, no_timing, trans));
   1.102  
   1.103 -val no_timing =
   1.104 -  map_transition (fn (name, props, pos, source, int_only, print, _, trans) =>
   1.105 -    (name, props, pos, source, int_only, print, true, trans));
   1.106 +val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
   1.107 +  (name, pos, source, int_only, print, true, trans));
   1.108  
   1.109 -fun add_trans tr =
   1.110 -  map_transition (fn (name, props, pos, source, int_only, print, no_timing, trans) =>
   1.111 -    (name, props, pos, source, int_only, print, no_timing, trans @ [tr]));
   1.112 +fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   1.113 +  (name, pos, source, int_only, print, no_timing, trans @ [tr]));
   1.114  
   1.115 -fun print' mode =
   1.116 -  map_transition (fn (name, props, pos, source, int_only, print, no_timing, trans) =>
   1.117 -    (name, props, pos, source, int_only, insert (op =) mode print, no_timing, trans));
   1.118 +fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   1.119 +  (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
   1.120  
   1.121  val print = print' "";
   1.122  
   1.123 @@ -566,9 +542,8 @@
   1.124  fun local_theory_presentation loc f g = app_current (fn int =>
   1.125    (fn Theory (gthy, _) =>
   1.126          let
   1.127 -          val pos = ContextPosition.get (Context.proof_of gthy);
   1.128            val finish = loc_finish loc gthy;
   1.129 -          val lthy' = f (ContextPosition.put_ctxt pos (loc_begin loc gthy));
   1.130 +          val lthy' = f (loc_begin loc gthy);
   1.131          in Theory (finish lthy', SOME lthy') end
   1.132      | _ => raise UNDEF) #> tap (g int));
   1.133  
   1.134 @@ -617,9 +592,7 @@
   1.135  in
   1.136  
   1.137  fun local_theory_to_proof' loc f = begin_proof
   1.138 -  (fn int => fn gthy =>
   1.139 -    f int (ContextPosition.put_ctxt (ContextPosition.get (Context.proof_of gthy))
   1.140 -      (loc_begin loc gthy)))
   1.141 +  (fn int => fn gthy => f int (loc_begin loc gthy))
   1.142    (loc_finish loc);
   1.143  
   1.144  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
   1.145 @@ -667,9 +640,9 @@
   1.146  
   1.147  (** toplevel transactions **)
   1.148  
   1.149 -(* thread transition properties *)
   1.150 +(* thread position *)
   1.151  
   1.152 -fun setmp_thread_position (Transition {props, pos, ...}) f x =
   1.153 +fun setmp_thread_position (Transition {pos, ...}) f x =
   1.154    Position.setmp_thread_data pos f x;
   1.155  
   1.156