# HG changeset patch
# User wenzelm
# Date 1492526098 -7200
# Node ID 741fad555d8288ed571697ec9d358b05b145d346
# Parent  b80477da30ebb441014021bca9a91a5a0c10ecf5
exclude theories from other sessions;
clarified modules;

diff -r b80477da30eb -r 741fad555d82 NEWS
--- a/NEWS	Tue Apr 18 14:51:46 2017 +0200
+++ b/NEWS	Tue Apr 18 16:34:58 2017 +0200
@@ -16,6 +16,9 @@
 contrast, a theory that is imported in the old-fashioned manner via an
 explicit file-system path belongs to the current session.
 
+Theories that are imported from other sessions are excluded from the
+current session document.
+
 * The main theory entry points for some non-HOL sessions have changed,
 to avoid confusion with the global name "Main" of the session HOL. This
 leads to the follow renamings:
diff -r b80477da30eb -r 741fad555d82 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Apr 18 16:34:58 2017 +0200
@@ -121,6 +121,9 @@
   into the current ML process, which is in contrast to a theory that is
   already present in the \<^emph>\<open>parent\<close> session.
 
+  Theories that are imported from other sessions are excluded from the current
+  session document.
+
   \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
   are processed within an environment that is augmented by the given options,
   in addition to the global session options given before. Any number of blocks
diff -r b80477da30eb -r 741fad555d82 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Apr 18 16:34:58 2017 +0200
@@ -18,6 +18,7 @@
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
+  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
   val import_name: string -> Path.T -> string ->
@@ -29,10 +30,6 @@
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
-  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
-    Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
-    theory * (unit -> unit) * int
 end;
 
 structure Resources: RESOURCES =
@@ -101,7 +98,10 @@
 val master_directory = #master_dir o Files.get;
 val imports_of = #imports o Files.get;
 
-fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
+fun begin_theory master_dir {name, imports, keywords} parents =
+  Theory.begin_theory name parents
+  |> map_files (fn _ => (master_dir, imports, []))
+  |> Thy_Header.add_keywords keywords;
 
 
 (* theory files *)
@@ -199,67 +199,6 @@
       | SOME ((_, id'), _) => id = id'));
 
 
-(* load theory *)
-
-fun begin_theory master_dir {name, imports, keywords} parents =
-  Theory.begin_theory name parents
-  |> put_deps master_dir imports
-  |> Thy_Header.add_keywords keywords;
-
-fun excursion keywords master_dir last_timing init elements =
-  let
-    fun prepare_span st span =
-      Command_Span.content span
-      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
-      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
-
-    fun element_result span_elem (st, _) =
-      let
-        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
-        val (results, st') = Toplevel.element_result keywords elem st;
-        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
-      in (results, (st', pos')) end;
-
-    val (results, (end_state, end_pos)) =
-      fold_map element_result elements (Toplevel.toplevel, Position.none);
-
-    val thy = Toplevel.end_theory end_pos end_state;
-  in (results, thy) end;
-
-fun load_thy document symbols last_timing update_time master_dir header text_pos text parents =
-  let
-    val (name, _) = #name header;
-    val keywords =
-      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
-        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
-
-    val toks = Token.explode keywords text_pos text;
-    val spans = Outer_Syntax.parse_spans toks;
-    val elements = Thy_Syntax.parse_elements keywords spans;
-
-    fun init () =
-      begin_theory master_dir header parents
-      |> Present.begin_theory update_time
-        (fn () => implode (map (HTML.present_span symbols keywords) spans));
-
-    val (results, thy) =
-      cond_timeit true ("theory " ^ quote name)
-        (fn () => excursion keywords master_dir last_timing init elements);
-
-    fun present () =
-      let
-        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
-      in
-        if exists (Toplevel.is_skipped_proof o #2) res then
-          warning ("Cannot present theory with skipped proofs: " ^ quote name)
-        else
-          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
-          in if document then Present.theory_output (Long_Name.base_name name) tex_source else () end
-      end;
-
-  in (thy, present, size text) end;
-
-
 (* antiquotations *)
 
 local
diff -r b80477da30eb -r 741fad555d82 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Pure/ROOT.ML	Tue Apr 18 16:34:58 2017 +0200
@@ -283,11 +283,11 @@
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
-ML_file "Thy/present.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
+ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/protocol_message.ML";
diff -r b80477da30eb -r 741fad555d82 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Pure/Thy/present.ML	Tue Apr 18 16:34:58 2017 +0200
@@ -12,7 +12,7 @@
   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
   val finish: unit -> unit
-  val theory_output: string -> string -> unit
+  val theory_output: theory -> string -> unit
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
   val display_drafts: Path.T list -> int
 end;
@@ -133,6 +133,10 @@
 
 fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
 
+fun is_session_theory thy =
+  (case ! session_info of
+    NONE => false
+  | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy));
 
 
 (** document preparation **)
@@ -280,9 +284,12 @@
 
 (* theory elements *)
 
-fun theory_output name s =
+fun theory_output thy tex =
   with_session_info () (fn _ =>
-    change_theory_info name (fn (_, html_source) => (Latex.isabelle_theory name s, html_source)));
+    if is_session_theory thy then
+      let val name = Context.theory_name thy;
+      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end
+    else ());
 
 fun theory_link (curr_chapter, curr_session) thy =
   let
@@ -300,18 +307,20 @@
   with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
     let
       val name = Context.theory_name thy;
-      val parents = Theory.parents_of thy;
 
-      val parent_specs = parents |> map (fn parent =>
-        (Option.map Url.File (theory_link (chapter, session_name) parent),
-          (Context.theory_name parent)));
+      val parent_specs =
+        Theory.parents_of thy |> map (fn parent =>
+          (Option.map Url.File (theory_link (chapter, session_name) parent),
+            (Context.theory_name parent)));
       val html_source = HTML.theory symbols name parent_specs (mk_text ());
-    in
-      init_theory_info name (make_theory_info ("", html_source));
-      add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
-      add_tex_index (update_time, Latex.theory_entry name);
-      Browser_Info.put {chapter = chapter, name = session_name} thy
-    end);
+      val _ = init_theory_info name (make_theory_info ("", html_source));
+
+      val _ =
+        if is_session_theory thy then
+          (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
+           add_tex_index (update_time, Latex.theory_entry name))
+        else ();
+    in Browser_Info.put {chapter = chapter, name = session_name} thy end);
 
 
 
diff -r b80477da30eb -r 741fad555d82 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 18 14:51:46 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 18 16:34:58 2017 +0200
@@ -230,6 +230,62 @@
 end;
 
 
+(* eval theory *)
+
+fun excursion keywords master_dir last_timing init elements =
+  let
+    fun prepare_span st span =
+      Command_Span.content span
+      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
+      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
+
+    fun element_result span_elem (st, _) =
+      let
+        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
+        val (results, st') = Toplevel.element_result keywords elem st;
+        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
+      in (results, (st', pos')) end;
+
+    val (results, (end_state, end_pos)) =
+      fold_map element_result elements (Toplevel.toplevel, Position.none);
+
+    val thy = Toplevel.end_theory end_pos end_state;
+  in (results, thy) end;
+
+fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents =
+  let
+    val (name, _) = #name header;
+    val keywords =
+      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
+        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
+
+    val toks = Token.explode keywords text_pos text;
+    val spans = Outer_Syntax.parse_spans toks;
+    val elements = Thy_Syntax.parse_elements keywords spans;
+
+    fun init () =
+      Resources.begin_theory master_dir header parents
+      |> Present.begin_theory update_time
+        (fn () => implode (map (HTML.present_span symbols keywords) spans));
+
+    val (results, thy) =
+      cond_timeit true ("theory " ^ quote name)
+        (fn () => excursion keywords master_dir last_timing init elements);
+
+    fun present () =
+      let
+        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
+      in
+        if exists (Toplevel.is_skipped_proof o #2) res then
+          warning ("Cannot present theory with skipped proofs: " ^ quote name)
+        else
+          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
+          in if document then Present.theory_output thy tex_source else () end
+      end;
+
+  in (thy, present, size text) end;
+
+
 (* require_thy -- checking database entries wrt. the file-system *)
 
 local
@@ -257,7 +313,7 @@
 
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
-      Resources.load_thy document symbols last_timing update_time dir header text_pos text
+      eval_thy document symbols last_timing update_time dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in