src/Pure/Thy/present.ML
changeset 66037 58d2e41afbfe
parent 65505 741fad555d82
child 66680 74a1b722507e
     1.1 --- a/src/Pure/Thy/present.ML	Thu Jun 08 12:25:59 2017 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Jun 08 12:54:55 2017 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature PRESENT =
     1.6  sig
     1.7 -  val session_name: theory -> string
     1.8 +  val theory_qualifier: theory -> string
     1.9    val document_enabled: string -> bool
    1.10    val document_variants: string -> (string * string) list
    1.11    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
    1.12 @@ -51,8 +51,6 @@
    1.13  val _ = Theory.setup
    1.14    (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
    1.15  
    1.16 -val session_name = #name o Browser_Info.get;
    1.17 -
    1.18  
    1.19  
    1.20  (** global browser info state **)
    1.21 @@ -133,10 +131,12 @@
    1.22  
    1.23  fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
    1.24  
    1.25 +val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;
    1.26 +
    1.27  fun is_session_theory thy =
    1.28    (case ! session_info of
    1.29      NONE => false
    1.30 -  | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy));
    1.31 +  | SOME {name, ...} => name = theory_qualifier thy);
    1.32  
    1.33  
    1.34  (** document preparation **)