# HG changeset patch # User desharna # Date 1608534945 -3600 # Node ID 5fa7f098ded5b9709188c53af3bd41dbdb403283 # Parent f931a2a68ab822b85a88e2451a6359d4c5496cbc# Parent 11de287ed4810bdd5bd767b328f93222fa60c5cd merged diff -r 11de287ed481 -r 5fa7f098ded5 NEWS --- 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. diff -r 11de287ed481 -r 5fa7f098ded5 etc/isabelle.css --- 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; } diff -r 11de287ed481 -r 5fa7f098ded5 src/Doc/JEdit/JEdit.thy --- 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>\CS\ 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. \ diff -r 11de287ed481 -r 5fa7f098ded5 src/HOL/Data_Structures/Binomial_Heap.thy --- 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 \ 'a tree \ nat" where [simp]: "T_link _ _ = 1" +text \This function is non-canonical: we omitted a \+1\ in the \else\-part, + to keep the following analysis simpler and more to the point. +\ fun T_ins_tree :: "'a::linorder tree \ 'a heap \ 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 \ 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) \ T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2 - )" + ) + 1" lemma T_del_min_bound: fixes ts defines "n \ size (mset_heap ts)" assumes "invar ts" and "ts\[]" - shows "T_del_min ts \ 6 * log 2 (n+1) + 2" + shows "T_del_min ts \ 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 \ts\[]\] 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 \ 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 \ 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 \ 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 \ 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 \n\<^sub>1 + n\<^sub>2 \ n\ also note \n\<^sub>1 \ n\ diff -r 11de287ed481 -r 5fa7f098ded5 src/HOL/Library/Word.thy --- 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 @@ \ \\unat_arith_tac\: tactic to reduce word arithmetic to \nat\, try to solve via \arith\\ ML \ 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} diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/General/path.scala --- 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 */ diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Isar/interpretation.ML --- 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 diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Isar/local_theory.ML --- 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; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Isar/locale.ML --- 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 ***) diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Isar/named_target.ML --- 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; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Isar/target_context.ML --- 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; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/command.ML --- 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 ""; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/command.scala --- 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) diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/command_span.scala --- 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) = diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/document.ML --- 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; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/document.scala --- 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) } } diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/protocol.ML --- 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); diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/protocol.scala --- 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) } } diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/resources.scala --- 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 */ diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/PIDE/session.scala --- 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 diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/ROOT.ML --- 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" - diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/System/isabelle_system.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; diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Thy/bibtex.scala --- 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 } diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Thy/file_format.scala --- 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 */ diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Thy/presentation.scala --- 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 **/ diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Tools/build.scala --- 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 = diff -r 11de287ed481 -r 5fa7f098ded5 src/Pure/Tools/build_job.scala --- 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()) diff -r 11de287ed481 -r 5fa7f098ded5 src/Tools/Argo/argo_proof.ML --- 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. diff -r 11de287ed481 -r 5fa7f098ded5 src/Tools/Argo/argo_thy.ML --- 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. *) diff -r 11de287ed481 -r 5fa7f098ded5 src/Tools/VSCode/src/preview_panel.scala --- 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 diff -r 11de287ed481 -r 5fa7f098ded5 src/Tools/jEdit/src/document_model.scala --- 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() diff -r 11de287ed481 -r 5fa7f098ded5 src/Tools/jEdit/src/jedit_rendering.scala --- 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)