# HG changeset patch # User wenzelm # Date 1672263466 -3600 # Node ID 4e97da5befc66254b39d0bdf446a7f542ac8e7f5 # Parent 18e719c6b6333841781af7bf09cb309e11b813d4# Parent 25900fbea7ad158282bfd532f146b0a10951f182 merged diff -r 18e719c6b633 -r 4e97da5befc6 src/HOL/SPARK/Tools/spark.scala --- a/src/HOL/SPARK/Tools/spark.scala Wed Dec 28 12:15:25 2022 +0000 +++ b/src/HOL/SPARK/Tools/spark.scala Wed Dec 28 22:37:46 2022 +0100 @@ -11,10 +11,12 @@ object SPARK { class Load_Command1 extends Command_Span.Load_Command("spark_vcg", Scala_Project.here) { + override def toString: String = print_extensions override val extensions: List[String] = List("vcg", "fdl", "rls") } class Load_Command2 extends Command_Span.Load_Command("spark_siv", Scala_Project.here) { + override def toString: String = print_extensions override val extensions: List[String] = List("siv", "fdl", "rls") } } diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/Isar/method.ML Wed Dec 28 22:37:46 2022 +0100 @@ -667,7 +667,7 @@ (keyword_positions text); fun report text_range = - if Context_Position.pide_reports () + if Context_Position.reports_enabled0 () then Position.reports (reports_of text_range) else (); end; diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/ML/ml_compiler.ML Wed Dec 28 22:37:46 2022 +0100 @@ -53,7 +53,7 @@ val reports_enabled = (case Context.get_generic_context () of SOME context => Context_Position.reports_enabled_generic context - | NONE => Context_Position.pide_reports ()); + | NONE => Context_Position.reports_enabled0 ()); fun is_reported pos = reports_enabled andalso Position.is_reported pos; diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/PIDE/command.ML Wed Dec 28 22:37:46 2022 +0100 @@ -7,7 +7,6 @@ signature COMMAND = sig type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option} - val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob Exn.result list * int -> Token.T list -> Toplevel.transition @@ -57,38 +56,6 @@ type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}; -fun read_file_node file_node master_dir pos delimited src_path = - let - val _ = - if Context_Position.pide_reports () - then Position.report pos (Markup.language_path delimited) else (); - - fun read_local () = - 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_remote () = - let - val text = Bytes.content (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 => read_local () - | SOME (Url.File _) => read_local () - | _ => read_remote ()); - - val lines = split_lines text; - val digest = SHA1.digest text; - 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 ""; - local fun blob_file src_path lines digest file_node = @@ -110,12 +77,14 @@ val pos = Input.pos_of source; val delimited = Input.is_delimited source; - fun make_file (Exn.Res {file_node, src_path, content = NONE}) = - Exn.interruptible_capture (fn () => - read_file_node file_node master_dir pos delimited src_path) () - | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) = - (Position.report pos (Markup.language_path delimited); - Exn.Res (blob_file src_path lines digest file_node)) + fun make_file (Exn.Res {file_node, src_path, content}) = + let val _ = Position.report pos (Markup.language_path delimited) in + case content of + NONE => + Exn.interruptible_capture (fn () => + Resources.read_file_node file_node master_dir (src_path, pos)) () + | SOME (digest, lines) => Exn.Res (blob_file src_path lines digest file_node) + end | make_file (Exn.Exn e) = Exn.Exn e; val files = map make_file blobs; in diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/PIDE/command_span.scala Wed Dec 28 22:37:46 2022 +0100 @@ -21,7 +21,15 @@ abstract class Load_Command(val name: String, val here: Scala_Project.Here) extends Isabelle_System.Service { - override def toString: String = name + override def toString: String = print("") + + def print(body: String): String = + if (body.nonEmpty) "Load_Command(" + body + ")" + else if (name.nonEmpty) print("name = " + quote(name)) + else "Load_Command" + + def print_extensions: String = + print("name = " + quote(name) + ", extensions = " + commas_quote(extensions)) def position: Position.T = here.position diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/PIDE/resources.ML Wed Dec 28 22:37:46 2022 +0100 @@ -37,10 +37,14 @@ val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} + val read_file_node: string -> Path.T -> Path.T * Position.T -> Token.file + val parsed_files: (Path.T -> Path.T list) -> + Token.file Exn.result list * Input.source -> theory -> Token.file list val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory + val provide_file': Token.file -> theory -> Token.file * theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool @@ -326,24 +330,55 @@ end; +(* read_file_node *) + +fun read_file_node file_node master_dir (src_path, pos) = + let + fun read_local () = + 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_remote () = + let + val text = Bytes.content (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 => read_local () + | SOME (Url.File _) => read_local () + | _ => read_remote ()); + + val lines = split_lines text; + val digest = SHA1.digest text; + 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); + + (* load files *) +fun parsed_files make_paths (files, source) thy = + if null files then + let + val master_dir = master_directory thy; + val name = Input.string_of source; + val pos = Input.pos_of source; + val delimited = Input.is_delimited source; + val src_paths = make_paths (Path.explode name); + val reports = + src_paths |> maps (fn src_path => + [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))), + (pos, Markup.language_path delimited)]); + val _ = Position.reports reports; + in map (read_file_node "" master_dir o rpair pos) src_paths end + else map Exn.release files; + fun parse_files make_paths = - Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => - (case Token.get_files tok of - [] => - let - val master_dir = master_directory thy; - val name = Input.string_of source; - val pos = Input.pos_of source; - val delimited = Input.is_delimited source; - val src_paths = make_paths (Path.explode name); - val reports = - src_paths |> map (fn src_path => - (pos, Markup.path (Path.implode_symbolic (master_dir + src_path)))); - val _ = Position.reports reports; - in map (Command.read_file master_dir pos delimited) src_paths end - | files => map Exn.release files)); + (Scan.ahead Parse.not_eof >> Token.get_files) -- Parse.path_input >> parsed_files make_paths; val parse_file = parse_files single >> (fn f => f #> the_single); @@ -355,13 +390,10 @@ else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); +fun provide_file' file thy = (file, provide_file file thy); fun provide_parse_files make_paths = - parse_files make_paths >> (fn files => fn thy => - let - val fs = files thy; - val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; - in (fs, thy') end); + parse_files make_paths >> (fn files => fn thy => fold_map provide_file' (files thy) thy); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); @@ -383,7 +415,7 @@ (* formal check *) -fun formal_check check_file ctxt opt_dir source = +fun formal_check (check: Path.T -> Path.T) ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; @@ -399,7 +431,7 @@ val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); - val _ : Path.T = check_file path handle ERROR msg => err msg; + val _ = check path handle ERROR msg => err msg; in path end; val check_path = formal_check I; diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/ROOT.ML Wed Dec 28 22:37:46 2022 +0100 @@ -311,9 +311,9 @@ ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; +ML_file "PIDE/resources.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; -ML_file "PIDE/resources.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/System/isabelle_process.ML Wed Dec 28 22:37:46 2022 +0100 @@ -118,7 +118,7 @@ in message name pos_props [XML.blob ss] end; fun report_message ss = - if Context_Position.pide_reports () + if Context_Position.reports_enabled0 () then standard_message [] Markup.reportN ss else (); val serial_props = Markup.serial_properties o serial; diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/Tools/generated_files.ML Wed Dec 28 22:37:46 2022 +0100 @@ -285,10 +285,9 @@ fun check_external_files ctxt (raw_files, raw_base_dir) = let val base_dir = Resources.check_dir ctxt NONE raw_base_dir; - fun check source = + val files = raw_files |> map (fn source => (Resources.check_file ctxt (SOME base_dir) source; - Path.explode (Input.string_of source)); - val files = map check raw_files; + Path.explode (Input.string_of source))); in (files, base_dir) end; fun get_external_files dir (files, base_dir) = diff -r 18e719c6b633 -r 4e97da5befc6 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Wed Dec 28 12:15:25 2022 +0000 +++ b/src/Pure/context_position.ML Wed Dec 28 22:37:46 2022 +0100 @@ -17,7 +17,7 @@ val restore_visible_generic: Context.generic -> Context.generic -> Context.generic val restore_visible: Proof.context -> Proof.context -> Proof.context val restore_visible_global: theory -> theory -> theory - val pide_reports: unit -> bool + val reports_enabled0: unit -> bool val reports_enabled_generic: Context.generic -> bool val reports_enabled: Proof.context -> bool val reports_enabled_global: theory -> bool @@ -64,9 +64,8 @@ (* PIDE reports *) -fun pide_reports () = Options.default_bool "pide_reports"; - -fun reports_enabled_generic context = pide_reports () andalso is_visible_generic context; +fun reports_enabled0 () = Options.default_bool "pide_reports"; +fun reports_enabled_generic context = reports_enabled0 () andalso is_visible_generic context; val reports_enabled = reports_enabled_generic o Context.Proof; val reports_enabled_global = reports_enabled_generic o Context.Theory;