more official session qualifier;
authorwenzelm
Thu Jun 08 12:54:55 2017 +0200 (23 months ago)
changeset 6603758d2e41afbfe
parent 66036 b6396880b644
child 66038 36bf57d6c011
more official session qualifier;
src/Pure/Thy/present.ML
src/Pure/Tools/thm_deps.ML
     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 **)
     2.1 --- a/src/Pure/Tools/thm_deps.ML	Thu Jun 08 12:25:59 2017 +0200
     2.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Jun 08 12:54:55 2017 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4                  a :: _ =>
     2.5                    (case try (Context.get_theory thy) a of
     2.6                      SOME thy =>
     2.7 -                      (case Present.session_name thy of
     2.8 +                      (case Present.theory_qualifier thy of
     2.9                          "" => []
    2.10                        | session => [session])
    2.11                    | NONE => [])