--- a/NEWS Thu Dec 17 15:31:31 2020 +0100
+++ b/NEWS Mon Dec 21 08:15:45 2020 +0100
@@ -16,6 +16,12 @@
*** Isabelle/jEdit Prover IDE ***
+* Improved markup for theory header imports: hyperlinks for theory files
+work without formal checking of content.
+
+* The prover process can download auxiliary files (e.g. 'ML_file') for
+theories with remote URL. This requires the external "curl" program.
+
* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
of the formal entity at the caret position.
--- a/etc/isabelle.css Thu Dec 17 15:31:31 2020 +0100
+++ b/etc/isabelle.css Mon Dec 21 08:15:45 2020 +0100
@@ -20,7 +20,7 @@
font-family: "Isabelle DejaVu Sans Mono", monospace;
}
-.theories { background-color: #FFFFFF; padding: 10px; }
+.contents { background-color: #FFFFFF; padding: 10px; }
.sessions { background-color: #FFFFFF; padding: 10px; }
.document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; }
--- a/src/Doc/JEdit/JEdit.thy Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Dec 21 08:15:45 2020 +0100
@@ -1317,7 +1317,8 @@
within the visible text area. The keyboard modifier \<^verbatim>\<open>CS\<close> overrides this:
then all defining and referencing positions are shown. This modifier may be
configured via option @{system_option jedit_focus_modifier}; the default
- coincides with the modifier for the above keyboard actions.
+ coincides with the modifier for the above keyboard actions. The empty string
+ means to disable this additional visual feedback.
\<close>
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Thu Dec 17 15:31:31 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Mon Dec 21 08:15:45 2020 +0100
@@ -478,6 +478,9 @@
definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
[simp]: "T_link _ _ = 1"
+text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
+ to keep the following analysis simpler and more to the point.
+\<close>
fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
"T_ins_tree t [] = 1"
| "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
@@ -603,13 +606,13 @@
definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where
"T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
\<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
- )"
+ ) + 1"
lemma T_del_min_bound:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
assumes "invar ts" and "ts\<noteq>[]"
- shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2"
+ shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
proof -
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
by (metis surj_pair tree.exhaust_sel)
@@ -625,7 +628,7 @@
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
by (auto simp: mset_heap_def)
- have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
+ have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1"
unfolding T_del_min_def GM
by simp
also have "T_get_min_rest ts \<le> log 2 (n+1)"
@@ -634,7 +637,7 @@
unfolding T_rev_def n\<^sub>1_def using size_mset_heap[OF I1] by simp
also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
- finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 2"
+ finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3"
by (simp add: algebra_simps)
also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close>
also note \<open>n\<^sub>1 \<le> n\<close>
--- a/src/HOL/Library/Word.thy Thu Dec 17 15:31:31 2020 +0100
+++ b/src/HOL/Library/Word.thy Mon Dec 21 08:15:45 2020 +0100
@@ -3227,7 +3227,8 @@
\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
ML \<open>
val unat_arith_simpset =
- @{context}
+ @{context} (* TODO: completely explicitly determined simpset *)
+ |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int}
|> fold Simplifier.add_simp @{thms unat_arith_simps}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
--- a/src/Pure/General/path.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/General/path.scala Mon Dec 21 08:15:45 2020 +0100
@@ -67,6 +67,15 @@
case Parent => ".."
}
+ private def squash_elem(elem: Elem): String =
+ elem match {
+ case Root("") => "ROOT"
+ case Root(s) => "SERVER_" + s
+ case Basic(s) => s
+ case Variable(s) => s
+ case Parent => "PARENT"
+ }
+
/* path constructors */
@@ -201,6 +210,7 @@
}
def xz: Path = ext("xz")
+ def html: Path = ext("html")
def tex: Path = ext("tex")
def pdf: Path = ext("pdf")
def thy: Path = ext("thy")
@@ -234,6 +244,8 @@
def drop_ext: Path = split_ext._1
def get_ext: String = split_ext._2
+ def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem))))
+
/* expand */
--- a/src/Pure/Isar/interpretation.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Isar/interpretation.ML Mon Dec 21 08:15:45 2020 +0100
@@ -156,13 +156,16 @@
(* interpretation in local theories *)
+val add_registration_local_theory =
+ Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
fun interpretation_cmd expression =
generic_interpretation read_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
(* interpretation into global theories *)
@@ -219,7 +222,7 @@
fun register_or_activate lthy =
if Named_Target.is_theory lthy
then Local_Theory.theory_registration
- else Locale.add_registration_local_theory;
+ else add_registration_local_theory;
fun gen_isar_interpretation prep_interpretation expression lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs
--- a/src/Pure/Isar/local_theory.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Isar/local_theory.ML Mon Dec 21 08:15:45 2020 +0100
@@ -24,7 +24,6 @@
type operations
val assert: local_theory -> local_theory
val level: Proof.context -> int
- val mark_brittle: local_theory -> local_theory
val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val background_naming_of: local_theory -> Name_Space.naming
val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -69,7 +68,6 @@
conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
- val exit_global_nonbrittle: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
val begin_nested: local_theory -> Binding.scope * local_theory
@@ -105,12 +103,11 @@
{background_naming: Name_Space.naming,
operations: operations,
conclude: Proof.context -> Proof.context,
- brittle: bool,
target: Proof.context};
-fun make_lthy (background_naming, operations, conclude, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, conclude, target) : lthy =
{background_naming = background_naming, operations = operations,
- conclude = conclude, brittle = brittle, target = target};
+ conclude = conclude, target = target};
(* context data *)
@@ -150,16 +147,16 @@
fun map_top f =
assert #>
- Data.map (fn {background_naming, operations, conclude, brittle, target} :: parents =>
- make_lthy (f (background_naming, operations, conclude, brittle, target)) :: parents);
+ Data.map (fn {background_naming, operations, conclude, target} :: parents =>
+ make_lthy (f (background_naming, operations, conclude, target)) :: parents);
fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
fun map_contexts f lthy =
let val n = level lthy in
lthy |> (Data.map o map_index)
- (fn (i, {background_naming, operations, conclude, brittle, target}) =>
- make_lthy (background_naming, operations, conclude, brittle,
+ (fn (i, {background_naming, operations, conclude, target}) =>
+ make_lthy (background_naming, operations, conclude,
target
|> Context_Position.set_visible false
|> f (n - i - 1)
@@ -168,26 +165,13 @@
end;
-(* brittle context -- implicit for nested structures *)
-
-fun mark_brittle lthy =
- if level lthy = 1 then
- map_top (fn (background_naming, operations, conclude, _, target) =>
- (background_naming, operations, conclude, true, target)) lthy
- else lthy;
-
-fun assert_nonbrittle lthy =
- if #brittle (top_of lthy) then error "Brittle local theory context"
- else lthy;
-
-
(* naming for background theory *)
val background_naming_of = #background_naming o top_of;
fun map_background_naming f =
- map_top (fn (background_naming, operations, conclude, brittle, target) =>
- (f background_naming, operations, conclude, brittle, target));
+ map_top (fn (background_naming, operations, conclude, target) =>
+ (f background_naming, operations, conclude, target));
val restore_background_naming = map_background_naming o K o background_naming_of;
@@ -353,8 +337,7 @@
(* main target *)
fun init_target background_naming conclude operations target =
- Data.map (K [make_lthy
- (background_naming, operations, conclude, false, target)]) target
+ Data.map (K [make_lthy (background_naming, operations, conclude, target)]) target
fun init {background_naming, setup, conclude} operations thy =
thy
@@ -366,7 +349,6 @@
fun exit lthy = exit_of lthy (assert_bottom lthy);
val exit_global = Proof_Context.theory_of o exit;
-val exit_global_nonbrittle = exit_global o assert_nonbrittle;
fun exit_result decl (x, lthy) =
let
@@ -389,7 +371,7 @@
val _ = assert lthy;
val (scope, target) = Proof_Context.new_scope lthy;
val entry = make_lthy (background_naming_of lthy, operations_of lthy,
- Proof_Context.restore_naming lthy, true, target);
+ Proof_Context.restore_naming lthy, target);
val lthy' = Data.map (cons entry) target;
in (scope, lthy') end;
--- a/src/Pure/Isar/locale.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Isar/locale.ML Mon Dec 21 08:15:45 2020 +0100
@@ -615,16 +615,13 @@
val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
-fun add_registration_local_theory' registration lthy =
+fun add_registration_local_theory registration lthy =
let val n = Local_Theory.level lthy in
lthy
|> Local_Theory.map_contexts (fn level =>
level = n - 1 ? Context.proof_map (add_registration registration))
end;
-fun add_registration_local_theory registration =
- Local_Theory.mark_brittle #> add_registration_local_theory' registration
-
fun add_registration_proof registration ctxt = ctxt
|> Proof_Context.set_stmt false
|> Context.proof_map (add_registration registration)
@@ -658,7 +655,7 @@
fun add_dependency loc registration =
Local_Theory.raw_theory (add_dependency' loc registration)
- #> add_registration_local_theory' registration;
+ #> add_registration_local_theory registration;
(*** Storing results ***)
--- a/src/Pure/Isar/named_target.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Isar/named_target.ML Mon Dec 21 08:15:45 2020 +0100
@@ -16,7 +16,8 @@
val theory_map: (local_theory -> local_theory) -> theory -> theory
val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
theory -> 'b * theory
- val reinit: local_theory -> theory -> local_theory
+ val revoke_reinitializability: local_theory -> local_theory
+ val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory
end;
structure Named_Target: NAMED_TARGET =
@@ -48,11 +49,11 @@
structure Data = Proof_Data
(
- type T = target option;
+ type T = (target * bool) option;
fun init _ = NONE;
);
-val get_bottom_target = Data.get;
+val get_bottom_target = Option.map fst o Data.get;
fun get_target lthy =
if Local_Theory.level lthy = 1
@@ -72,6 +73,9 @@
val class_of = class_of_target o get_target;
+fun is_reinitializable lthy =
+ Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy;
+
(* operations *)
@@ -115,6 +119,11 @@
| setup_context (Locale locale) = Locale.init locale
| setup_context (Class class) = Class.init class;
+fun setup target includes =
+ setup_context target
+ #> Data.put (SOME (target, null includes))
+ #> Bundle.includes includes;
+
fun init includes ident thy =
let
val target = target_of_ident thy ident;
@@ -122,10 +131,9 @@
thy
|> Local_Theory.init
{background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
- setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes,
+ setup = setup target includes,
conclude = I}
(operations target)
- |> not (null includes) ? Local_Theory.mark_brittle
end;
val theory_init = init [] "";
@@ -134,6 +142,11 @@
fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
-fun reinit lthy = init [] (ident_of lthy);
+val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false);
+
+fun exit_global_reinitialize lthy =
+ if is_reinitializable lthy
+ then (init [] (ident_of lthy), Local_Theory.exit_global lthy)
+ else error "Non-reinitializable local theory context";
end;
--- a/src/Pure/Isar/target_context.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Isar/target_context.ML Mon Dec 21 08:15:45 2020 +0100
@@ -36,8 +36,12 @@
| switch_named_cmd NONE (Context.Proof lthy) =
(Context.Proof o Local_Theory.reset, lthy)
| switch_named_cmd (SOME name) (Context.Proof lthy) =
- (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
- (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy);
+ let
+ val (reinit, thy) = Named_Target.exit_global_reinitialize lthy
+ in
+ (Context.Proof o reinit o Local_Theory.exit_global,
+ context_begin_named_cmd [] name thy)
+ end;
fun includes raw_includes lthy =
Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;
--- a/src/Pure/PIDE/command.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/command.ML Mon Dec 21 08:15:45 2020 +0100
@@ -60,19 +60,29 @@
val _ =
if Context_Position.pide_reports ()
then Position.report pos (Markup.language_path delimited) else ();
- val _ =
+
+ fun read_file () =
+ let
+ val path = File.check_file (File.full_path master_dir src_path);
+ val text = File.read path;
+ val file_pos = Path.position path;
+ in (text, file_pos) end;
+
+ fun read_url () =
+ let
+ val text = Isabelle_System.download file_node;
+ val file_pos = Position.file file_node;
+ in (text, file_pos) end;
+
+ val (text, file_pos) =
(case try Url.explode file_node of
- NONE => ()
- | SOME (Url.File _) => ()
- | _ =>
- error ("Prover cannot load remote file " ^
- Markup.markup (Markup.path file_node) (quote file_node)));
- val full_path = File.check_file (File.full_path master_dir src_path);
- val text = File.read full_path;
+ NONE => read_file ()
+ | SOME (Url.File _) => read_file ()
+ | _ => read_url ());
+
val lines = split_lines text;
val digest = SHA1.digest text;
- val file_pos = Position.copy_id pos (Path.position full_path);
- in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
+ in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end
handle ERROR msg => error (msg ^ Position.here pos);
val read_file = read_file_node "";
--- a/src/Pure/PIDE/command.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/command.scala Mon Dec 21 08:15:45 2020 +0100
@@ -30,7 +30,7 @@
src_path: Path,
content: Option[(SHA1.Digest, Symbol.Text_Chunk)])
{
- def read_file: String = File.read(name.path)
+ def read_file: Bytes = Bytes.read(name.path)
def chunk_file: Symbol.Text_Chunk.File =
Symbol.Text_Chunk.File(name.node)
@@ -445,8 +445,8 @@
span.name match {
// inlined errors
case Thy_Header.THEORY =>
- val reader = Scan.char_reader(Token.implode(span.content))
- val header = resources.check_thy(node_name, reader)
+ val reader = span.content_reader
+ val header = resources.check_thy(node_name, span.content_reader)
val imports_pos = header.imports_pos
val raw_imports =
try {
@@ -567,6 +567,23 @@
def source(range: Text.Range): String = range.substring(source)
+ /* theory parents */
+
+ def theory_parents(resources: Resources): List[Document.Node.Name] =
+ if (span.name == Thy_Header.THEORY) {
+ try {
+ val header = Thy_Header.read(node_name, span.content_reader)
+ for ((s, _) <- header.imports)
+ yield {
+ try { resources.import_name(node_name, s) }
+ catch { case ERROR(_) => Document.Node.Name.empty }
+ }
+ }
+ catch { case ERROR(_) => Nil }
+ }
+ else Nil
+
+
/* reported positions */
def reported_position(pos: Position.T)
--- a/src/Pure/PIDE/command_span.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Mon Dec 21 08:15:45 2020 +0100
@@ -8,6 +8,7 @@
import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
object Command_Span
@@ -89,6 +90,8 @@
def is_begin: Boolean = content.exists(_.is_begin)
def is_end: Boolean = content.exists(_.is_end)
+ def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
+
def length: Int = (0 /: content)(_ + _.source.length)
def compact_source: (String, Span) =
--- a/src/Pure/PIDE/document.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/document.ML Mon Dec 21 08:15:45 2020 +0100
@@ -22,6 +22,7 @@
type command =
{command_id: Document_ID.command,
name: string,
+ parents: string list,
blobs_digests: blob_digest list,
blobs_index: int,
tokens: ((int * int) * string) list}
@@ -410,11 +411,12 @@
type command =
{command_id: Document_ID.command,
name: string,
+ parents: string list,
blobs_digests: blob_digest list,
blobs_index: int,
tokens: ((int * int) * string) list};
-fun define_command {command_id, name, blobs_digests, blobs_index, tokens} =
+fun define_command {command_id, name, parents, blobs_digests, blobs_index, tokens} =
map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
@@ -424,6 +426,24 @@
(fn () =>
let
val (tokens, _) = fold_map Token.make tokens (Position.id id);
+ val imports =
+ if name = Thy_Header.theoryN then
+ (#imports (Thy_Header.read_tokens Position.none tokens)
+ handle ERROR _ => [])
+ else [];
+ val _ =
+ if length parents = length imports then
+ (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
+ let val markup =
+ (case Thy_Info.lookup_theory parent of
+ SOME thy => Theory.get_markup thy
+ | NONE =>
+ (case try Url.explode parent of
+ NONE => Markup.path parent
+ | SOME (Url.File path) => Markup.path (Path.implode path)
+ | SOME _ => Markup.path parent))
+ in Position.report pos markup end)
+ else ();
val _ =
if blobs_index < 0
then (*inlined errors*)
@@ -598,8 +618,8 @@
(case get_result (snd (the (AList.lookup (op =) deps import))) of
NONE => Toplevel.init_toplevel ()
| SOME (_, eval) => maybe_eval_result eval)
- | some => some)
- |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
+ |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))
+ | SOME thy => SOME (thy, (Position.none, Markup.empty))));
val parents =
if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
--- a/src/Pure/PIDE/document.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/document.scala Mon Dec 21 08:15:45 2020 +0100
@@ -592,7 +592,7 @@
/* command as add-on snippet */
- def command_snippet(command: Command): Snapshot =
+ def snippet(command: Command): Snapshot =
{
val node_name = command.node_name
@@ -620,16 +620,23 @@
elements: Markup.Elements = Markup.Elements.full): XML.Body =
state.xml_markup(version, node_name, range = range, elements = elements)
- def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] =
+ def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full)
+ : List[(Path, XML.Body)] =
{
snippet_command match {
case None => Nil
case Some(command) =>
for (Exn.Res(blob) <- command.blobs)
yield {
- val text = blob.read_file
- val markup = command.init_markups(Command.Markup_Index.blob(blob))
- markup.to_XML(Text.Range(0, text.length), text, elements)
+ val bytes = blob.read_file
+ val text = bytes.text
+ val xml =
+ if (Bytes(text) == bytes) {
+ val markup = command.init_markups(Command.Markup_Index.blob(blob))
+ markup.to_XML(Text.Range(0, text.length), text, elements)
+ }
+ else Nil
+ blob.src_path -> xml
}
}
}
@@ -998,8 +1005,7 @@
Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
blobs_info = command.blobs_info, results = st.results, markups = st.markups)
val state1 = copy(theories = theories - id)
- val snapshot = state1.command_snippet(command1)
- (snapshot, state1)
+ (state1.snippet(command1), state1)
}
def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
@@ -1252,7 +1258,7 @@
new Snapshot(this, version, node_name, edits, snippet_command)
}
- def command_snippet(command: Command): Snapshot =
- snapshot().command_snippet(command)
+ def snippet(command: Command): Snapshot =
+ snapshot().snippet(command)
}
}
--- a/src/Pure/PIDE/protocol.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Mon Dec 21 08:15:45 2020 +0100
@@ -31,9 +31,10 @@
Isabelle_Process.protocol_command "Document.define_blob"
(fn [digest, content] => Document.change_state (Document.define_blob digest content));
-fun decode_command id name blobs_xml toks_xml sources : Document.command =
+fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
let
open XML.Decode;
+ val parents = list string parents_xml;
val (blobs_digests, blobs_index) =
blobs_xml |>
let
@@ -52,6 +53,7 @@
in
{command_id = Document_ID.parse id,
name = name,
+ parents = parents,
blobs_digests = blobs_digests,
blobs_index = blobs_index,
tokens = toks ~~ sources}
@@ -62,9 +64,11 @@
val _ =
Isabelle_Process.protocol_command "Document.define_command"
- (fn id :: name :: blobs :: toks :: sources =>
+ (fn id :: name :: parents :: blobs :: toks :: sources =>
let
- val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources;
+ val command =
+ decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs)
+ (YXML.parse_body toks) sources;
val _ = Document.change_state (Document.define_command command);
in commands_accepted [id] end);
@@ -75,9 +79,10 @@
fun decode arg =
let
open XML.Decode;
- val (id, (name, (blobs_xml, (toks_xml, sources)))) =
- pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg);
- in decode_command id name blobs_xml toks_xml sources end;
+ val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) =
+ pair string (pair string (pair I (pair I (pair I (list string)))))
+ (YXML.parse_body arg);
+ in decode_command id name parents_xml blobs_xml toks_xml sources end;
val commands = map decode args;
val _ = Document.change_state (fold Document.define_command commands);
--- a/src/Pure/PIDE/protocol.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Dec 21 08:15:45 2020 +0100
@@ -321,10 +321,14 @@
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
- private def encode_command(command: Command): (String, String, String, String, List[String]) =
+ private def encode_command(resources: Resources, command: Command)
+ : (String, String, String, String, String, List[String]) =
{
import XML.Encode._
+ val parents = command.theory_parents(resources).map(name => File.standard_url(name.node))
+ val parents_yxml = Symbol.encode_yxml(list(string)(parents))
+
val blobs_yxml =
{
val encode_blob: T[Exn.Result[Command.Blob]] =
@@ -344,38 +348,42 @@
}
val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
- (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources)
+ (Document_ID(command.id), Symbol.encode(command.span.name), parents_yxml,
+ blobs_yxml, toks_yxml, toks_sources)
}
- def define_command(command: Command)
+ def define_command(resources: Resources, command: Command)
{
- val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
+ val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
+ encode_command(resources, command)
protocol_command_args(
- "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources)
+ "Document.define_command", command_id :: name :: parents_yxml :: blobs_yxml ::
+ toks_yxml :: toks_sources)
}
- def define_commands(commands: List[Command])
+ def define_commands(resources: Resources, commands: List[Command])
{
protocol_command_args("Document.define_commands",
commands.map(command =>
{
import XML.Encode._
- val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
+ val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
+ encode_command(resources, command)
val body =
- pair(string, pair(string, pair(string, pair(string, list(string)))))(
- command_id, (name, (blobs_yxml, (toks_yxml, toks_sources))))
+ pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))(
+ command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources)))))
YXML.string_of_body(body)
}))
}
- def define_commands_bulk(commands: List[Command])
+ def define_commands_bulk(resources: Resources, commands: List[Command])
{
val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
- irregular.foreach(define_command)
+ irregular.foreach(define_command(resources, _))
regular match {
case Nil =>
- case List(command) => define_command(command)
- case _ => define_commands(regular)
+ case List(command) => define_command(resources, command)
+ case _ => define_commands(resources, regular)
}
}
--- a/src/Pure/PIDE/resources.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Dec 21 08:15:45 2020 +0100
@@ -12,6 +12,12 @@
import java.io.{File => JFile}
+object Resources
+{
+ def empty: Resources =
+ new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+}
+
class Resources(
val sessions_structure: Sessions.Structure,
val session_base: Sessions.Base,
@@ -54,12 +60,12 @@
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
- def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
- File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
-
def is_hidden(name: Document.Node.Name): Boolean =
!name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
+ File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
+
/* file-system operations */
--- a/src/Pure/PIDE/session.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/PIDE/session.scala Mon Dec 21 08:15:45 2020 +0100
@@ -452,7 +452,9 @@
for { (_, edit) <- change.doc_edits } {
edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
}
- if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList)
+ if (id_commands.nonEmpty) {
+ prover.get.define_commands_bulk(resources, id_commands.toList)
+ }
}
val assignment = global_state.value.the_assignment(change.previous).check_finished
--- a/src/Pure/ROOT.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 21 08:15:45 2020 +0100
@@ -354,4 +354,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
-
--- a/src/Pure/System/isabelle_system.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/System/isabelle_system.ML Mon Dec 21 08:15:45 2020 +0100
@@ -20,6 +20,7 @@
val create_tmp_path: string -> string -> Path.T
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
+ val download: string -> string
end;
structure Isabelle_System: ISABELLE_SYSTEM =
@@ -29,7 +30,7 @@
fun bash_output_check s =
(case Bash.process s of
- {rc = 0, out, ...} => (trim_line out)
+ {rc = 0, out, ...} => trim_line out
| {err, ...} => error (trim_line err));
fun bash_output s =
@@ -120,4 +121,14 @@
let val path = create_tmp_path name ""
in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
+
+(* download file *)
+
+fun download url =
+ with_tmp_file "download" "" (fn path =>
+ ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
+ |> Bash.process
+ |> (fn {rc = 0, ...} => File.read path
+ | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
+
end;
--- a/src/Pure/Thy/bibtex.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Thy/bibtex.scala Mon Dec 21 08:15:45 2020 +0100
@@ -30,7 +30,7 @@
"""theory "bib" imports Pure begin bibtex_file """ +
Outer_Syntax.quote_string(name) + """ end"""
- override def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
+ override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
{
val name = snapshot.node_name
if (detect(name.node)) {
@@ -40,7 +40,7 @@
File.write(bib, snapshot.node.source)
Bibtex.html_output(List(bib), style = "unsort", title = title)
}
- Some(Presentation.Preview(title, content))
+ Some(Presentation.HTML_Document(title, content))
}
else None
}
--- a/src/Pure/Thy/file_format.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Thy/file_format.scala Mon Dec 21 08:15:45 2020 +0100
@@ -89,7 +89,7 @@
} yield s
}
- def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = None
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = None
/* PIDE session agent */
--- a/src/Pure/Thy/presentation.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Mon Dec 21 08:15:45 2020 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/present.scala
Author: Makarius
-Theory presentation: HTML and LaTeX documents.
+HTML/PDF presentation of theory documents.
*/
package isabelle
@@ -12,6 +12,127 @@
object Presentation
{
+ /** HTML documents **/
+
+ val fonts_path = Path.explode("fonts")
+
+ sealed case class HTML_Document(title: String, content: String)
+
+ def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context =
+ new HTML_Context(fonts_url)
+
+ final class HTML_Context private[Presentation](fonts_url: String => String)
+ {
+ def init_fonts(dir: Path)
+ {
+ val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
+ for (entry <- Isabelle_Fonts.fonts(hidden = true))
+ File.copy(entry.path, fonts_dir)
+ }
+
+ def head(title: String, rest: XML.Body = Nil): XML.Tree =
+ HTML.div("head", HTML.chapter(title) :: rest)
+
+ def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
+
+ def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
+ : List[XML.Elem] =
+ {
+ if (items.isEmpty) Nil
+ else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
+ }
+
+ def output_document(title: String, body: XML.Body): String =
+ HTML.output_document(
+ List(
+ HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
+ HTML.title(title)),
+ List(HTML.source(body)), css = "", structural = false)
+
+ def html_document(title: String, body: XML.Body): HTML_Document =
+ HTML_Document(title, output_document(title, body))
+ }
+
+
+ /* HTML body */
+
+ private val div_elements =
+ Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
+ HTML.descr.name)
+
+ private def html_div(html: XML.Body): Boolean =
+ html exists {
+ case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
+ case XML.Text(_) => false
+ }
+
+ private def html_class(c: String, html: XML.Body): XML.Tree =
+ if (html.forall(_ == HTML.no_text)) HTML.no_text
+ else if (html_div(html)) HTML.div(c, html)
+ else HTML.span(c, html)
+
+ private def html_body(xml: XML.Body): XML.Body =
+ xml map {
+ case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
+ html_class(Markup.Language.DOCUMENT, html_body(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
+ case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
+ case XML.Elem(Markup.Markdown_List(kind), body) =>
+ if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body))
+ case XML.Elem(markup, body) =>
+ val name = markup.name
+ val html =
+ markup.properties match {
+ case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
+ List(html_class(kind, html_body(body)))
+ case _ =>
+ html_body(body)
+ }
+ Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+ case Some(c) => html_class(c.toString, html)
+ case None => html_class(name, html)
+ }
+ case XML.Text(text) =>
+ XML.Text(Symbol.decode(text))
+ }
+
+
+ /* PIDE HTML document */
+
+ val html_elements: Markup.Elements =
+ Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
+ Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
+
+ def html_document(
+ resources: Resources,
+ snapshot: Document.Snapshot,
+ html_context: HTML_Context,
+ plain_text: Boolean = false): HTML_Document =
+ {
+ require(!snapshot.is_outdated)
+
+ val name = snapshot.node_name
+ if (plain_text) {
+ val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
+ val body = HTML.text(snapshot.node.source)
+ html_context.html_document(title, body)
+ }
+ else {
+ resources.html_document(snapshot) getOrElse {
+ val title =
+ if (name.is_theory) "Theory " + quote(name.theory_base_name)
+ else "File " + Symbol.cartouche_decoded(name.path.file_name)
+ val body = html_body(snapshot.xml_markup(elements = html_elements))
+ html_context.html_document(title, body)
+ }
+ }
+ }
+
+
+
+ /** PDF LaTeX documents **/
+
/* document info */
abstract class Document_Name
@@ -152,7 +273,10 @@
}
- /* maintain chapter index -- NOT thread-safe */
+
+ /** HTML presentation **/
+
+ /* maintain chapter index */
private val sessions_path = Path.basic(".sessions")
@@ -215,10 +339,10 @@
/* present session */
val session_graph_path = Path.explode("session_graph.pdf")
- val readme_path = Path.basic("README.html")
+ val readme_path = Path.explode("README.html")
+ val files_path = Path.explode("files")
def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
- def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = {
if (keywords.is_command(tok, Keyword.theory_end))
@@ -246,9 +370,11 @@
}
def session_html(
+ resources: Resources,
session: String,
deps: Sessions.Deps,
db_context: Sessions.Database_Context,
+ html_context: HTML_Context,
presentation: Context)
{
val info = deps.sessions_structure(session)
@@ -256,9 +382,8 @@
val base = deps(session)
val session_dir = presentation.dir(db_context.store, info)
- val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
- for (entry <- Isabelle_Fonts.fonts(hidden = true))
- File.copy(entry.path, session_fonts)
+
+ html_context.init_fonts(session_dir)
Bytes.write(session_dir + session_graph_path,
graphview.Graph_File.make_pdf(options, base.session_graph_display))
@@ -300,6 +425,39 @@
HTML.link(prefix + html_name(name1), body)
}
+ val files: List[XML.Body] =
+ {
+ var seen_files = List.empty[(Path, String, Document.Node.Name)]
+ (for {
+ thy_name <- base.session_theories.iterator
+ thy_command <-
+ Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator
+ snapshot = Document.State.init.snippet(thy_command)
+ (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
+ if xml.nonEmpty
+ } yield {
+ val file_title = src_path.implode_short
+ val file_name = (files_path + src_path.squash.html).implode
+
+ seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
+ case None => seen_files ::= (src_path, file_name, thy_name)
+ case Some((_, _, thy_name1)) =>
+ error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
+ " in theory " + thy_name1 + " vs. " + thy_name)
+ }
+
+ val file_path = session_dir + Path.explode(file_name)
+ html_context.init_fonts(file_path.dir)
+
+ val title = "File " + Symbol.cartouche_decoded(file_title)
+ HTML.write_document(file_path.dir, file_path.file_name,
+ List(HTML.title(title)),
+ List(html_context.head(title), html_context.source(html_body(xml))))
+
+ List(HTML.link(file_name, HTML.text(file_title)))
+ }).toList
+ }
+
val theories =
for (name <- base.session_theories)
yield {
@@ -334,7 +492,7 @@
val title = "Theory " + name.theory_base_name
HTML.write_document(session_dir, html_name(name),
List(HTML.title(title)),
- HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body)))
+ List(html_context.head(title), html_context.source(thy_body)))
List(HTML.link(html_name(name), HTML.text(name.theory_base_name)))
}
@@ -342,104 +500,12 @@
val title = "Session " + session
HTML.write_document(session_dir, "index.html",
List(HTML.title(title + " (" + Distribution.version + ")")),
- HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
- (if (theories.isEmpty) Nil
- else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories))))))
- }
-
-
-
- /** preview **/
-
- sealed case class Preview(title: String, content: String)
-
- def preview(
- resources: Resources,
- snapshot: Document.Snapshot,
- plain_text: Boolean = false,
- fonts_url: String => String = HTML.fonts_url()): Preview =
- {
- require(!snapshot.is_outdated)
-
- def output_document(title: String, body: XML.Body): String =
- HTML.output_document(
- List(
- HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
- HTML.title(title)),
- List(HTML.source(body)), css = "", structural = false)
-
- val name = snapshot.node_name
-
- if (plain_text) {
- val title = "File " + quote(name.path.file_name)
- val content = output_document(title, HTML.text(snapshot.node.source))
- Preview(title, content)
- }
- else {
- resources.make_preview(snapshot) match {
- case Some(preview) => preview
- case None =>
- val title =
- if (name.is_theory) "Theory " + quote(name.theory_base_name)
- else "File " + quote(name.path.file_name)
- val content = output_document(title, pide_document(snapshot))
- Preview(title, content)
- }
- }
+ html_context.head(title, List(HTML.par(links))) ::
+ html_context.contents("Theories", theories) :::
+ html_context.contents("Files", files))
}
- /* PIDE document */
-
- private val document_elements =
- Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
- Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
-
- private val div_elements =
- Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
- HTML.descr.name)
-
- private def html_div(html: XML.Body): Boolean =
- html exists {
- case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
- case XML.Text(_) => false
- }
-
- private def html_class(c: String, html: XML.Body): XML.Tree =
- if (html.forall(_ == HTML.no_text)) HTML.no_text
- else if (html_div(html)) HTML.div(c, html)
- else HTML.span(c, html)
-
- private def make_html(xml: XML.Body): XML.Body =
- xml map {
- case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
- html_class(Markup.Language.DOCUMENT, make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
- case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
- case XML.Elem(Markup.Markdown_List(kind), body) =>
- if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
- case XML.Elem(markup, body) =>
- val name = markup.name
- val html =
- markup.properties match {
- case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
- List(html_class(kind, make_html(body)))
- case _ =>
- make_html(body)
- }
- Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
- case Some(c) => html_class(c.toString, html)
- case None => html_class(name, html)
- }
- case XML.Text(text) =>
- XML.Text(Symbol.decode(text))
- }
-
- def pide_document(snapshot: Document.Snapshot): XML.Body =
- make_html(snapshot.xml_markup(elements = document_elements))
-
-
/** build documents **/
--- a/src/Pure/Tools/build.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Tools/build.scala Mon Dec 21 08:15:45 2020 +0100
@@ -502,11 +502,15 @@
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
+ val resources = Resources.empty
+ val html_context = Presentation.html_context()
+
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
progress.expose_interrupt()
progress.echo("Presenting " + session_name + " ...")
- Presentation.session_html(session_name, deps, db_context, presentation)
+ Presentation.session_html(
+ resources, session_name, deps, db_context, html_context, presentation)
})
val browser_chapters =
--- a/src/Pure/Tools/build_job.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Dec 21 08:15:45 2020 +0100
@@ -30,8 +30,7 @@
(read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
case (Value.Long(id), thy_file :: blobs_files) =>
- val thy_path = Path.explode(thy_file)
- val node_name = resources.file_node(thy_path, theory = theory)
+ val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
val results =
Command.Results.make(
@@ -43,7 +42,7 @@
{
val path = Path.explode(file)
val name = resources.file_node(path)
- val src_path = File.relative_path(thy_path, path).getOrElse(path)
+ val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
Command.Blob(name, src_path, None)
})
val blobs_xml =
@@ -94,7 +93,7 @@
{
val store = Sessions.store(options)
- val resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+ val resources = Resources.empty
val session = new Session(options, resources)
using(store.open_database_context())(db_context =>
@@ -120,7 +119,7 @@
match {
case None => progress.echo(thy_heading + " MISSING")
case Some(command) =>
- val snapshot = Document.State.init.command_snippet(command)
+ val snapshot = Document.State.init.snippet(command)
val rendering = new Rendering(snapshot, options, session)
val messages =
rendering.text_messages(Text.Range.full)
@@ -376,7 +375,7 @@
export_text(Export.FILES,
cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
- for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) {
+ for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
export(Export.MARKUP + (i + 1), xml)
}
export(Export.MARKUP, snapshot.xml_markup())
--- a/src/Tools/Argo/argo_proof.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Tools/Argo/argo_proof.ML Mon Dec 21 08:15:45 2020 +0100
@@ -7,7 +7,7 @@
The proof language is inspired by:
- Leonardo de Moura and Nikolaj Bj/orner. Proofs and Refutations, and Z3. In
+ Leonardo de Moura and Nikolaj Bjørner. Proofs and Refutations, and Z3. In
Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof
Assistants, and the 7th International Workshop on the Implementation of Logics,
volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
--- a/src/Tools/Argo/argo_thy.ML Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Tools/Argo/argo_thy.ML Mon Dec 21 08:15:45 2020 +0100
@@ -9,7 +9,7 @@
Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. In ACM
Transactions on Programming Languages and Systems, 1(2):245-257, 1979.
- Leonardo de Moura and Nikolaj Bj/orner. Model-based Theory Combination. In Electronic Notes
+ Leonardo de Moura and Nikolaj Bjørner. Model-based Theory Combination. In Electronic Notes
in Theoretical Computer Science, volume 198(2), pages 37-49, 2008.
*)
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Mon Dec 21 08:15:45 2020 +0100
@@ -30,8 +30,9 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val preview = Presentation.preview(resources, snapshot)
- channel.write(LSP.Preview_Response(file, column, preview.title, preview.content))
+ val html_context = Presentation.html_context()
+ val document = Presentation.html_document(resources, snapshot, html_context)
+ channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
case None => m - file
--- a/src/Tools/jEdit/src/document_model.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 21 08:15:45 2020 +0100
@@ -16,7 +16,7 @@
import scala.collection.mutable
import scala.annotation.tailrec
-import org.gjt.sp.jedit.{jEdit, View}
+import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
@@ -153,11 +153,11 @@
state.change_result(st =>
st.buffer_models.get(buffer) match {
case Some(buffer_model) if buffer_model.node_name == node_name =>
- buffer_model.init_token_marker
+ buffer_model.init_token_marker()
(buffer_model, st)
case _ =>
val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
- buffer.propertiesChanged
+ buffer.propertiesChanged()
res
})
}
@@ -168,7 +168,7 @@
state.change(st =>
if (st.buffer_models.isDefinedAt(buffer)) {
val res = st.close_buffer(buffer)
- buffer.propertiesChanged
+ buffer.propertiesChanged()
res
}
else st)
@@ -298,7 +298,7 @@
case Some(model) =>
val name = model.node_name
val url =
- PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
+ PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
@@ -310,7 +310,7 @@
val fonts_root = http_root + "/fonts"
val preview_root = http_root + "/preview"
- val preview =
+ val html =
HTTP.get(preview_root, arg =>
for {
query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
@@ -319,13 +319,14 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- val preview =
- Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+ val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
+ val document =
+ Presentation.html_document(PIDE.resources, snapshot, html_context,
plain_text = query.startsWith(plain_text_prefix))
- HTTP.Response.html(preview.content)
+ HTTP.Response.html(document.content)
})
- List(HTTP.fonts(fonts_root), preview)
+ List(HTTP.fonts(fonts_root), html)
}
}
@@ -642,7 +643,7 @@
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
- buffer.invalidateCachedFoldLevels
+ buffer.invalidateCachedFoldLevels()
}
def init_token_marker()
--- a/src/Tools/jEdit/src/jedit_rendering.scala Thu Dec 17 15:31:31 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Dec 21 08:15:45 2020 +0100
@@ -30,7 +30,7 @@
results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
{
val command = Command.rich_text(Document_ID.make(), results, formatted_body)
- val snippet = snapshot.command_snippet(command)
+ val snippet = snapshot.snippet(command)
val model = File_Model.empty(PIDE.session)
val rendering = apply(snippet, model, PIDE.options.value)
(command.source, rendering)