--- 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:
--- 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
--- 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
--- 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";
--- 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);
--- 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