removed obsolete context_position.ML (superseded by Position.thread_data);
authorwenzelm
Thu Jan 24 23:51:11 2008 +0100 (2008-01-24)
changeset 2595303937086b1fe
parent 25952 2152b47a87ed
child 25954 682e84b60e5c
removed obsolete context_position.ML (superseded by Position.thread_data);
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/context_position.ML
     1.1 --- a/src/Pure/IsaMakefile	Thu Jan 24 12:02:44 2008 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Thu Jan 24 23:51:11 2008 +0100
     1.3 @@ -70,13 +70,12 @@
     1.4    Tools/ROOT.ML Tools/invoke.ML Tools/isabelle_process.ML			\
     1.5    Tools/named_thms.ML Tools/xml_syntax.ML assumption.ML axclass.ML		\
     1.6    codegen.ML compress.ML config.ML conjunction.ML consts.ML context.ML		\
     1.7 -  context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
     1.8 -  fact_index.ML goal.ML interpretation.ML library.ML logic.ML			\
     1.9 -  meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML old_goals.ML	\
    1.10 -  pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML		\
    1.11 -  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML			\
    1.12 -  tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML			\
    1.13 -  type_infer.ML unify.ML variable.ML
    1.14 +  conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML		\
    1.15 +  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML		\
    1.16 +  morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
    1.17 +  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
    1.18 +  sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
    1.19 +  thm.ML type.ML type_infer.ML unify.ML variable.ML
    1.20  	@./mk
    1.21  
    1.22  
     2.1 --- a/src/Pure/ROOT.ML	Thu Jan 24 12:02:44 2008 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Thu Jan 24 23:51:11 2008 +0100
     2.3 @@ -26,7 +26,6 @@
     2.4  use "Syntax/lexicon.ML";
     2.5  use "Syntax/simple_syntax.ML";
     2.6  use "context.ML";
     2.7 -use "context_position.ML";
     2.8  use "sorts.ML";
     2.9  use "type.ML";
    2.10  use "type_infer.ML";
     3.1 --- a/src/Pure/context_position.ML	Thu Jan 24 12:02:44 2008 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,35 +0,0 @@
     3.4 -(*  Title:      Pure/context_position.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Context positions.
     3.9 -*)
    3.10 -
    3.11 -signature CONTEXT_POSITION =
    3.12 -sig
    3.13 -  val put: Position.T -> Context.generic -> Context.generic
    3.14 -  val put_ctxt: Position.T -> Proof.context -> Proof.context
    3.15 -  val get: Proof.context -> Position.T
    3.16 -  val str_of: Proof.context -> string
    3.17 -  val properties_of: Proof.context -> Markup.property list
    3.18 -end;
    3.19 -
    3.20 -structure ContextPosition: CONTEXT_POSITION =
    3.21 -struct
    3.22 -
    3.23 -structure Data = GenericDataFun
    3.24 -(
    3.25 -  type T = Position.T;
    3.26 -  val empty = Position.none;
    3.27 -  fun extend _ = empty;
    3.28 -  fun merge _ _ = empty;
    3.29 -);
    3.30 -
    3.31 -val put = Data.put;
    3.32 -val put_ctxt = Context.proof_map o put;
    3.33 -
    3.34 -val get = Data.get o Context.Proof;
    3.35 -val str_of = Position.str_of o get;
    3.36 -val properties_of = Position.properties_of o get;
    3.37 -
    3.38 -end;