src/Pure/Thy/present.ML
changeset 24561 7b4aa14d2491
parent 24150 ed724867099a
child 24829 e1214fa781ca
     1.1 --- a/src/Pure/Thy/present.ML	Sat Sep 08 19:58:36 2007 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Sep 08 19:58:37 2007 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  signature PRESENT =
     1.5  sig
     1.6    include BASIC_PRESENT
     1.7 -  val get_info: theory -> {name: string, session: string list, is_local: bool}
     1.8 +  val session_name: theory -> string
     1.9    val write_graph: {name: string, ID: string, dir: string, unfold: bool,
    1.10     path: string, parents: string list} list -> Path.T -> unit
    1.11    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    1.12 @@ -87,6 +87,8 @@
    1.13    then {name = Context.PureN, session = [], is_local = false}
    1.14    else BrowserInfoData.get thy;
    1.15  
    1.16 +val session_name = #name o get_info;
    1.17 +
    1.18  
    1.19  
    1.20  (** graphs **)
    1.21 @@ -102,7 +104,7 @@
    1.22  
    1.23  fun display_graph gr =
    1.24    let
    1.25 -    val _ = writeln "Generating graph ...";
    1.26 +    val _ = writeln "Displaying graph ...";
    1.27      val path = File.tmp_path (Path.explode "tmp.graph");
    1.28      val _ = write_graph gr path;
    1.29      val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");