--- a/src/Pure/Thy/present.ML Thu Jun 08 12:25:59 2017 +0200
+++ b/src/Pure/Thy/present.ML Thu Jun 08 12:54:55 2017 +0200
@@ -6,7 +6,7 @@
signature PRESENT =
sig
- val session_name: theory -> string
+ val theory_qualifier: theory -> string
val document_enabled: string -> bool
val document_variants: string -> (string * string) list
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -51,8 +51,6 @@
val _ = Theory.setup
(Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
-val session_name = #name o Browser_Info.get;
-
(** global browser info state **)
@@ -133,10 +131,12 @@
fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
+val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;
+
fun is_session_theory thy =
(case ! session_info of
NONE => false
- | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy));
+ | SOME {name, ...} => name = theory_qualifier thy);
(** document preparation **)
--- a/src/Pure/Tools/thm_deps.ML Thu Jun 08 12:25:59 2017 +0200
+++ b/src/Pure/Tools/thm_deps.ML Thu Jun 08 12:54:55 2017 +0200
@@ -29,7 +29,7 @@
a :: _ =>
(case try (Context.get_theory thy) a of
SOME thy =>
- (case Present.session_name thy of
+ (case Present.theory_qualifier thy of
"" => []
| session => [session])
| NONE => [])