--- 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")
}
}
--- 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;
--- 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;
--- 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
--- 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
--- 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;
--- 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";
--- 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;
--- 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) =
--- 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;