src/Pure/Thy/thm_deps.ML
changeset 7785 c06825c396e8
parent 7783 9ace4017ead8
child 7786 cf9d07ad62af
equal deleted inserted replaced
7784:228283fa5de4 7785:c06825c396e8
     3     Author:     Stefan Berghofer, TU Muenchen
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     4 
     5 Visualize dependencies of theorems.
     5 Visualize dependencies of theorems.
     6 *)
     6 *)
     7 
     7 
       
     8 signature BASIC_THM_DEPS =
       
     9 sig
       
    10   val thm_deps : thm list -> unit
       
    11 end;
       
    12 
     8 signature THM_DEPS =
    13 signature THM_DEPS =
     9 sig
    14 sig
    10   val thm_deps: thm list -> unit
    15   include BASIC_THM_DEPS
       
    16 
       
    17   val enable : unit -> unit
       
    18   val disable : unit -> unit
    11 end;
    19 end;
    12 
    20 
    13 structure ThmDeps : THM_DEPS =
    21 structure ThmDeps : THM_DEPS =
    14 struct
    22 struct
       
    23 
       
    24 fun enable () = Thm.keep_derivs := ThmDeriv;
       
    25 fun disable () = Thm.keep_derivs := MinDeriv;
    15 
    26 
    16 fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    27 fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    17   else
    28   else
    18     (case #session (Present.get_info thy) of
    29     (case #session (Present.get_info thy) of
    19         [x] => [x, "base"]
    30         [x] => [x, "base"]
    67     val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    78     val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    68   in () end;
    79   in () end;
    69 
    80 
    70 end;
    81 end;
    71 
    82 
    72 open ThmDeps;
    83 structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
       
    84 
       
    85 open BasicThmDeps;