exclude theories from other sessions;
authorwenzelm
Tue Apr 18 16:34:58 2017 +0200 (2017-04-18)
changeset 65505741fad555d82
parent 65504 b80477da30eb
child 65506 359fc6266a00
exclude theories from other sessions;
clarified modules;
NEWS
src/Doc/System/Sessions.thy
src/Pure/PIDE/resources.ML
src/Pure/ROOT.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/NEWS	Tue Apr 18 14:51:46 2017 +0200
     1.2 +++ b/NEWS	Tue Apr 18 16:34:58 2017 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4  contrast, a theory that is imported in the old-fashioned manner via an
     1.5  explicit file-system path belongs to the current session.
     1.6  
     1.7 +Theories that are imported from other sessions are excluded from the
     1.8 +current session document.
     1.9 +
    1.10  * The main theory entry points for some non-HOL sessions have changed,
    1.11  to avoid confusion with the global name "Main" of the session HOL. This
    1.12  leads to the follow renamings:
     2.1 --- a/src/Doc/System/Sessions.thy	Tue Apr 18 14:51:46 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Tue Apr 18 16:34:58 2017 +0200
     2.3 @@ -121,6 +121,9 @@
     2.4    into the current ML process, which is in contrast to a theory that is
     2.5    already present in the \<^emph>\<open>parent\<close> session.
     2.6  
     2.7 +  Theories that are imported from other sessions are excluded from the current
     2.8 +  session document.
     2.9 +
    2.10    \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
    2.11    are processed within an environment that is augmented by the given options,
    2.12    in addition to the global session options given before. Any number of blocks
     3.1 --- a/src/Pure/PIDE/resources.ML	Tue Apr 18 14:51:46 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Tue Apr 18 16:34:58 2017 +0200
     3.3 @@ -18,6 +18,7 @@
     3.4    val known_theory: string -> Path.T option
     3.5    val master_directory: theory -> Path.T
     3.6    val imports_of: theory -> (string * Position.T) list
     3.7 +  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     3.8    val thy_path: Path.T -> Path.T
     3.9    val theory_qualifier: string -> string
    3.10    val import_name: string -> Path.T -> string ->
    3.11 @@ -29,10 +30,6 @@
    3.12    val provide: Path.T * SHA1.digest -> theory -> theory
    3.13    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
    3.14    val loaded_files_current: theory -> bool
    3.15 -  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    3.16 -  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
    3.17 -    Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
    3.18 -    theory * (unit -> unit) * int
    3.19  end;
    3.20  
    3.21  structure Resources: RESOURCES =
    3.22 @@ -101,7 +98,10 @@
    3.23  val master_directory = #master_dir o Files.get;
    3.24  val imports_of = #imports o Files.get;
    3.25  
    3.26 -fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
    3.27 +fun begin_theory master_dir {name, imports, keywords} parents =
    3.28 +  Theory.begin_theory name parents
    3.29 +  |> map_files (fn _ => (master_dir, imports, []))
    3.30 +  |> Thy_Header.add_keywords keywords;
    3.31  
    3.32  
    3.33  (* theory files *)
    3.34 @@ -199,67 +199,6 @@
    3.35        | SOME ((_, id'), _) => id = id'));
    3.36  
    3.37  
    3.38 -(* load theory *)
    3.39 -
    3.40 -fun begin_theory master_dir {name, imports, keywords} parents =
    3.41 -  Theory.begin_theory name parents
    3.42 -  |> put_deps master_dir imports
    3.43 -  |> Thy_Header.add_keywords keywords;
    3.44 -
    3.45 -fun excursion keywords master_dir last_timing init elements =
    3.46 -  let
    3.47 -    fun prepare_span st span =
    3.48 -      Command_Span.content span
    3.49 -      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
    3.50 -      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    3.51 -
    3.52 -    fun element_result span_elem (st, _) =
    3.53 -      let
    3.54 -        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
    3.55 -        val (results, st') = Toplevel.element_result keywords elem st;
    3.56 -        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    3.57 -      in (results, (st', pos')) end;
    3.58 -
    3.59 -    val (results, (end_state, end_pos)) =
    3.60 -      fold_map element_result elements (Toplevel.toplevel, Position.none);
    3.61 -
    3.62 -    val thy = Toplevel.end_theory end_pos end_state;
    3.63 -  in (results, thy) end;
    3.64 -
    3.65 -fun load_thy document symbols last_timing update_time master_dir header text_pos text parents =
    3.66 -  let
    3.67 -    val (name, _) = #name header;
    3.68 -    val keywords =
    3.69 -      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
    3.70 -        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
    3.71 -
    3.72 -    val toks = Token.explode keywords text_pos text;
    3.73 -    val spans = Outer_Syntax.parse_spans toks;
    3.74 -    val elements = Thy_Syntax.parse_elements keywords spans;
    3.75 -
    3.76 -    fun init () =
    3.77 -      begin_theory master_dir header parents
    3.78 -      |> Present.begin_theory update_time
    3.79 -        (fn () => implode (map (HTML.present_span symbols keywords) spans));
    3.80 -
    3.81 -    val (results, thy) =
    3.82 -      cond_timeit true ("theory " ^ quote name)
    3.83 -        (fn () => excursion keywords master_dir last_timing init elements);
    3.84 -
    3.85 -    fun present () =
    3.86 -      let
    3.87 -        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    3.88 -      in
    3.89 -        if exists (Toplevel.is_skipped_proof o #2) res then
    3.90 -          warning ("Cannot present theory with skipped proofs: " ^ quote name)
    3.91 -        else
    3.92 -          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
    3.93 -          in if document then Present.theory_output (Long_Name.base_name name) tex_source else () end
    3.94 -      end;
    3.95 -
    3.96 -  in (thy, present, size text) end;
    3.97 -
    3.98 -
    3.99  (* antiquotations *)
   3.100  
   3.101  local
     4.1 --- a/src/Pure/ROOT.ML	Tue Apr 18 14:51:46 2017 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Tue Apr 18 16:34:58 2017 +0200
     4.3 @@ -283,11 +283,11 @@
     4.4  ML_file "Thy/thy_output.ML";
     4.5  ML_file "Thy/document_antiquotations.ML";
     4.6  ML_file "General/graph_display.ML";
     4.7 -ML_file "Thy/present.ML";
     4.8  ML_file "pure_syn.ML";
     4.9  ML_file "PIDE/command.ML";
    4.10  ML_file "PIDE/query_operation.ML";
    4.11  ML_file "PIDE/resources.ML";
    4.12 +ML_file "Thy/present.ML";
    4.13  ML_file "Thy/thy_info.ML";
    4.14  ML_file "PIDE/session.ML";
    4.15  ML_file "PIDE/protocol_message.ML";
     5.1 --- a/src/Pure/Thy/present.ML	Tue Apr 18 14:51:46 2017 +0200
     5.2 +++ b/src/Pure/Thy/present.ML	Tue Apr 18 16:34:58 2017 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     5.5      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
     5.6    val finish: unit -> unit
     5.7 -  val theory_output: string -> string -> unit
     5.8 +  val theory_output: theory -> string -> unit
     5.9    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    5.10    val display_drafts: Path.T list -> int
    5.11  end;
    5.12 @@ -133,6 +133,10 @@
    5.13  
    5.14  fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
    5.15  
    5.16 +fun is_session_theory thy =
    5.17 +  (case ! session_info of
    5.18 +    NONE => false
    5.19 +  | SOME {name, ...} => name = Resources.theory_qualifier (Context.theory_long_name thy));
    5.20  
    5.21  
    5.22  (** document preparation **)
    5.23 @@ -280,9 +284,12 @@
    5.24  
    5.25  (* theory elements *)
    5.26  
    5.27 -fun theory_output name s =
    5.28 +fun theory_output thy tex =
    5.29    with_session_info () (fn _ =>
    5.30 -    change_theory_info name (fn (_, html_source) => (Latex.isabelle_theory name s, html_source)));
    5.31 +    if is_session_theory thy then
    5.32 +      let val name = Context.theory_name thy;
    5.33 +      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end
    5.34 +    else ());
    5.35  
    5.36  fun theory_link (curr_chapter, curr_session) thy =
    5.37    let
    5.38 @@ -300,18 +307,20 @@
    5.39    with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
    5.40      let
    5.41        val name = Context.theory_name thy;
    5.42 -      val parents = Theory.parents_of thy;
    5.43  
    5.44 -      val parent_specs = parents |> map (fn parent =>
    5.45 -        (Option.map Url.File (theory_link (chapter, session_name) parent),
    5.46 -          (Context.theory_name parent)));
    5.47 +      val parent_specs =
    5.48 +        Theory.parents_of thy |> map (fn parent =>
    5.49 +          (Option.map Url.File (theory_link (chapter, session_name) parent),
    5.50 +            (Context.theory_name parent)));
    5.51        val html_source = HTML.theory symbols name parent_specs (mk_text ());
    5.52 -    in
    5.53 -      init_theory_info name (make_theory_info ("", html_source));
    5.54 -      add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
    5.55 -      add_tex_index (update_time, Latex.theory_entry name);
    5.56 -      Browser_Info.put {chapter = chapter, name = session_name} thy
    5.57 -    end);
    5.58 +      val _ = init_theory_info name (make_theory_info ("", html_source));
    5.59 +
    5.60 +      val _ =
    5.61 +        if is_session_theory thy then
    5.62 +          (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
    5.63 +           add_tex_index (update_time, Latex.theory_entry name))
    5.64 +        else ();
    5.65 +    in Browser_Info.put {chapter = chapter, name = session_name} thy end);
    5.66  
    5.67  
    5.68  
     6.1 --- a/src/Pure/Thy/thy_info.ML	Tue Apr 18 14:51:46 2017 +0200
     6.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Apr 18 16:34:58 2017 +0200
     6.3 @@ -230,6 +230,62 @@
     6.4  end;
     6.5  
     6.6  
     6.7 +(* eval theory *)
     6.8 +
     6.9 +fun excursion keywords master_dir last_timing init elements =
    6.10 +  let
    6.11 +    fun prepare_span st span =
    6.12 +      Command_Span.content span
    6.13 +      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
    6.14 +      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    6.15 +
    6.16 +    fun element_result span_elem (st, _) =
    6.17 +      let
    6.18 +        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
    6.19 +        val (results, st') = Toplevel.element_result keywords elem st;
    6.20 +        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    6.21 +      in (results, (st', pos')) end;
    6.22 +
    6.23 +    val (results, (end_state, end_pos)) =
    6.24 +      fold_map element_result elements (Toplevel.toplevel, Position.none);
    6.25 +
    6.26 +    val thy = Toplevel.end_theory end_pos end_state;
    6.27 +  in (results, thy) end;
    6.28 +
    6.29 +fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents =
    6.30 +  let
    6.31 +    val (name, _) = #name header;
    6.32 +    val keywords =
    6.33 +      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
    6.34 +        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
    6.35 +
    6.36 +    val toks = Token.explode keywords text_pos text;
    6.37 +    val spans = Outer_Syntax.parse_spans toks;
    6.38 +    val elements = Thy_Syntax.parse_elements keywords spans;
    6.39 +
    6.40 +    fun init () =
    6.41 +      Resources.begin_theory master_dir header parents
    6.42 +      |> Present.begin_theory update_time
    6.43 +        (fn () => implode (map (HTML.present_span symbols keywords) spans));
    6.44 +
    6.45 +    val (results, thy) =
    6.46 +      cond_timeit true ("theory " ^ quote name)
    6.47 +        (fn () => excursion keywords master_dir last_timing init elements);
    6.48 +
    6.49 +    fun present () =
    6.50 +      let
    6.51 +        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    6.52 +      in
    6.53 +        if exists (Toplevel.is_skipped_proof o #2) res then
    6.54 +          warning ("Cannot present theory with skipped proofs: " ^ quote name)
    6.55 +        else
    6.56 +          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
    6.57 +          in if document then Present.theory_output thy tex_source else () end
    6.58 +      end;
    6.59 +
    6.60 +  in (thy, present, size text) end;
    6.61 +
    6.62 +
    6.63  (* require_thy -- checking database entries wrt. the file-system *)
    6.64  
    6.65  local
    6.66 @@ -257,7 +313,7 @@
    6.67  
    6.68      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    6.69      val (theory, present, weight) =
    6.70 -      Resources.load_thy document symbols last_timing update_time dir header text_pos text
    6.71 +      eval_thy document symbols last_timing update_time dir header text_pos text
    6.72          (if name = Context.PureN then [Context.the_global_context ()] else parents);
    6.73      fun commit () = update_thy deps theory;
    6.74    in