# HG changeset patch # User wenzelm # Date 1395160743 -3600 # Node ID 06cc31dff1389d16cef6939bcd99cff6917ac3a6 # Parent 52d5067ca06a1bdc68ca8da32997954a5bfdcf78 clarifed module name; diff -r 52d5067ca06a -r 06cc31dff138 src/Doc/Codegen/Setup.thy --- a/src/Doc/Codegen/Setup.thy Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Doc/Codegen/Setup.thy Tue Mar 18 17:39:03 2014 +0100 @@ -9,7 +9,7 @@ (* FIXME avoid writing into source directory *) ML {* - Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples")) + Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples")) *} ML_file "../antiquote_setup.ML" diff -r 52d5067ca06a -r 06cc31dff138 src/Doc/Tutorial/ToyList/ToyList_Test.thy --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Mar 18 17:39:03 2014 +0100 @@ -5,7 +5,7 @@ ML {* (* FIXME somewhat non-standard, fragile *) let val texts = - map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) + map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) ["ToyList1", "ToyList2"]; val trs = Outer_Syntax.parse Position.start (implode texts); val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; diff -r 52d5067ca06a -r 06cc31dff138 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Tue Mar 18 17:39:03 2014 +0100 @@ -152,7 +152,7 @@ val _ = Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) (fn {context = ctxt, ...} => - fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]))); + fn name => (Resources.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]))); (* Isabelle/jEdit elements *) diff -r 52d5067ca06a -r 06cc31dff138 src/HOL/SMT_Examples/boogie.ML --- a/src/HOL/SMT_Examples/boogie.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/HOL/SMT_Examples/boogie.ML Tue Mar 18 17:39:03 2014 +0100 @@ -317,7 +317,7 @@ val _ = Outer_Syntax.command @{command_spec "boogie_file"} "prove verification condition from .b2i file" - (Thy_Load.provide_parse_files "boogie_file" >> (fn files => + (Resources.provide_parse_files "boogie_file" >> (fn files => Toplevel.theory (fn thy => let val ([{lines, ...}], thy') = files thy; diff -r 52d5067ca06a -r 06cc31dff138 src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Tue Mar 18 17:39:03 2014 +0100 @@ -12,7 +12,7 @@ val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file, {lines = fdl_lines, pos = fdl_pos, ...}, {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy; - val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path)); + val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path)); in SPARK_VCs.set_vcs (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))) @@ -24,7 +24,7 @@ (* FIXME *) fun spark_open_old (vc_name, prfx) thy = let - val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name); + val ((vc_path, vc_id), vc_text) = Resources.load_file thy (Path.explode vc_name); val (base, header) = (case Path.split_ext vc_path of (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) @@ -117,13 +117,13 @@ val _ = Outer_Syntax.command @{command_spec "spark_open_vcg"} "open a new SPARK environment and load a SPARK-generated .vcg file" - (Parse.parname -- Thy_Load.provide_parse_files "spark_open_vcg" + (Parse.parname -- Resources.provide_parse_files "spark_open_vcg" >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header)); val _ = Outer_Syntax.command @{command_spec "spark_open_siv"} "open a new SPARK environment and load a SPARK-generated .siv file" - (Parse.parname -- Thy_Load.provide_parse_files "spark_open_siv" + (Parse.parname -- Resources.provide_parse_files "spark_open_siv" >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header)); val pfun_type = Scan.option diff -r 52d5067ca06a -r 06cc31dff138 src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Tue Mar 18 17:39:03 2014 +0100 @@ -198,7 +198,7 @@ if name = "" then NONE else Path.explode name - |> Path.append (Thy_Load.master_directory (Context.theory_of context)) + |> Path.append (Resources.master_directory (Context.theory_of context)) |> SOME o Cache_IO.unsynchronized_init) val certificates_of = Certificates.get o Context.Proof diff -r 52d5067ca06a -r 06cc31dff138 src/HOL/Tools/SMT2/smt2_config.ML --- a/src/HOL/Tools/SMT2/smt2_config.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_config.ML Tue Mar 18 17:39:03 2014 +0100 @@ -195,7 +195,7 @@ if name = "" then NONE else Path.explode name - |> Path.append (Thy_Load.master_directory (Context.theory_of context)) + |> Path.append (Resources.master_directory (Context.theory_of context)) |> SOME o Cache_IO.unsynchronized_init) val certificates_of = Certificates.get o Context.Proof diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Isar/parse.scala Tue Mar 18 17:39:03 2014 +0100 @@ -64,7 +64,7 @@ def path: Parser[String] = atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content)) def theory_name: Parser[String] = - atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content)) + atom("theory name", tok => tok.is_name && Resources.is_wellformed_thy_path(tok.content)) private def tag_name: Parser[String] = atom("tag name", tok => diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/PIDE/document.ML Tue Mar 18 17:39:03 2014 +0100 @@ -443,7 +443,7 @@ NONE => Toplevel.toplevel | SOME eval => Command.eval_result_state eval))); val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); - in Thy_Load.begin_theory master_dir header parents end; + in Resources.begin_theory master_dir header parents end; fun check_theory full name node = is_some (loaded_theory name) orelse diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/PIDE/resources.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/resources.ML Tue Mar 18 17:39:03 2014 +0100 @@ -0,0 +1,243 @@ +(* Title: Pure/PIDE/resources.ML + Author: Makarius + +Resources for theories and auxiliary files. +*) + +signature RESOURCES = +sig + val master_directory: theory -> Path.T + val imports_of: theory -> (string * Position.T) list + val thy_path: Path.T -> Path.T + 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 parse_files: string -> (theory -> Token.file list) parser + val provide: Path.T * SHA1.digest -> theory -> theory + val provide_parse_files: string -> (theory -> Token.file list * theory) parser + val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string + val loaded_files: theory -> Path.T list + val loaded_files_current: theory -> bool + val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory + val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> + Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int +end; + +structure Resources: RESOURCES = +struct + +(* manage source files *) + +type files = + {master_dir: Path.T, (*master directory of theory source*) + imports: (string * Position.T) list, (*source specification of imports*) + provided: (Path.T * SHA1.digest) list}; (*source path, digest*) + +fun make_files (master_dir, imports, provided): files = + {master_dir = master_dir, imports = imports, provided = provided}; + +structure Files = Theory_Data +( + type T = files; + val empty = make_files (Path.current, [], []); + fun extend _ = empty; + fun merge _ = empty; +); + +fun map_files f = + Files.map (fn {master_dir, imports, provided} => + make_files (f (master_dir, imports, provided))); + + +val master_directory = #master_dir o Files.get; +val imports_of = #imports o Files.get; + +fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, [])); + + +(* theory files *) + +val thy_path = Path.ext "thy"; + +fun check_file dir file = File.check_file (File.full_path dir file); + +fun check_thy dir thy_name = + let + val path = thy_path (Path.basic thy_name); + val master_file = check_file dir path; + val text = File.read master_file; + + val {name = (name, pos), imports, keywords} = + Thy_Header.read (Path.position master_file) text; + val _ = thy_name <> name andalso + error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos); + in + {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, + imports = imports, keywords = keywords} + end; + + +(* load files *) + +fun parse_files cmd = + Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => + (case Token.get_files tok of + [] => + let + val master_dir = master_directory thy; + val pos = Token.pos_of tok; + val src_paths = Keyword.command_files cmd (Path.explode name); + in map (Command.read_file master_dir pos) src_paths end + | files => map Exn.release files)); + +fun provide (src_path, id) = + map_files (fn (master_dir, imports, provided) => + if AList.defined (op =) provided src_path then + error ("Duplicate use of source file: " ^ Path.print src_path) + else (master_dir, imports, (src_path, id) :: provided)); + +fun provide_parse_files cmd = + parse_files cmd >> (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); + +fun load_file thy src_path = + let + val full_path = check_file (master_directory thy) src_path; + val text = File.read full_path; + val id = SHA1.digest text; + in ((full_path, id), text) end; + +fun loaded_files_current thy = + #provided (Files.get thy) |> + forall (fn (src_path, id) => + (case try (load_file thy) src_path of + NONE => false + | SOME ((_, id'), _) => id = id')); + +(*Proof General legacy*) +fun loaded_files thy = + let val {master_dir, provided, ...} = Files.get thy + in map (File.full_path master_dir o #1) provided end; + + +(* load theory *) + +fun begin_theory master_dir {name, imports, keywords} parents = + Theory.begin_theory name parents + |> put_deps master_dir imports + |> fold Thy_Header.declare_keyword keywords; + +fun excursion master_dir last_timing init elements = + let + fun prepare_span span = + Thy_Syntax.span_content span + |> Command.read init master_dir [] + |> (fn tr => Toplevel.put_timing (last_timing tr) tr); + + fun element_result span_elem (st, _) = + let + val elem = Thy_Syntax.map_element prepare_span span_elem; + val (results, st') = Toplevel.element_result elem st; + val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); + in (results, (st', pos')) end; + + val (results, (end_state, end_pos)) = + fold_map element_result elements (Toplevel.toplevel, Position.none); + + val thy = Toplevel.end_theory end_pos end_state; + in (results, thy) end; + +fun load_thy document last_timing update_time master_dir header text_pos text parents = + let + val time = ! Toplevel.timing; + + val {name = (name, _), ...} = header; + val _ = Thy_Header.define_keywords header; + + val lexs = Keyword.get_lexicons (); + val toks = Thy_Syntax.parse_tokens lexs text_pos text; + val spans = Thy_Syntax.parse_spans toks; + val elements = Thy_Syntax.parse_elements spans; + + fun init () = + begin_theory master_dir header parents + |> Present.begin_theory update_time + (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); + + val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); + val (results, thy) = + cond_timeit time "" (fn () => excursion master_dir last_timing init elements); + val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); + + fun present () = + let + val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results); + val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); + in + if exists (Toplevel.is_skipped_proof o #2) res then + warning ("Cannot present theory with skipped proofs: " ^ quote name) + else + let val tex_source = + Thy_Output.present_thy minor Keyword.command_tags + (Outer_Syntax.is_markup outer_syntax) res toks + |> Buffer.content; + in if document then Present.theory_output name tex_source else () end + end; + + in (thy, present, size text) end; + + +(* antiquotations *) + +local + +fun check_path strict ctxt dir (name, pos) = + let + val _ = Context_Position.report ctxt pos Markup.language_path; + + val path = Path.append dir (Path.explode name) + handle ERROR msg => error (msg ^ Position.here pos); + + val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); + val _ = + if can Path.expand path andalso File.exists path then () + else + let + val path' = perhaps (try Path.expand) path; + val msg = "Bad file: " ^ Path.print path' ^ Position.here pos; + in + if strict then error msg + else + Context_Position.if_visible ctxt Output.report + (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg) + end; + in path end; + +fun file_antiq strict ctxt (name, pos) = + let + val dir = master_directory (Proof_Context.theory_of ctxt); + val _ = check_path strict ctxt dir (name, pos); + in + space_explode "/" name + |> map Thy_Output.verb_text + |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}") + end; + +in + +val _ = Theory.setup + (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path)) + (file_antiq true o #context) #> + Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path)) + (file_antiq false o #context) #> + ML_Antiquotation.value @{binding path} + (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) => + let val path = check_path true ctxt Path.current arg + in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end))); + +end; + +end; diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/PIDE/resources.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/resources.scala Tue Mar 18 17:39:03 2014 +0100 @@ -0,0 +1,111 @@ +/* Title: Pure/PIDE/resources.scala + Author: Makarius + +Resources for theories and auxiliary files. +*/ + +package isabelle + + +import scala.annotation.tailrec + +import java.io.{File => JFile} + + +object Resources +{ + /* paths */ + + def thy_path(path: Path): Path = path.ext("thy") + + def is_wellformed_thy_path(str: String): Boolean = + try { thy_path(Path.explode(str)); true } + catch { case ERROR(_) => false } +} + + +class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax) +{ + /* document node names */ + + def node_name(raw_path: Path): Document.Node.Name = + { + val path = raw_path.expand + val node = path.implode + val theory = Thy_Header.thy_name(node).getOrElse("") + val master_dir = if (theory == "") "" else path.dir.implode + Document.Node.Name(node, master_dir, theory) + } + + + /* file-system operations */ + + def append(dir: String, source_path: Path): String = + (Path.explode(dir) + source_path).expand.implode + + def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = + { + val path = Path.explode(name.node) + if (!path.is_file) error("No such file: " + path.toString) + + val text = File.read(path) + Symbol.decode_strict(text) + f(text) + } + + + /* theory files */ + + def body_files_test(syntax: Outer_Syntax, text: String): Boolean = + syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) + + def body_files(syntax: Outer_Syntax, text: String): List[String] = + { + val spans = Thy_Syntax.parse_spans(syntax.scan(text)) + spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList + } + + def import_name(master: Document.Node.Name, s: String): Document.Node.Name = + { + val theory = Thy_Header.base_name(s) + if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory) + else { + val path = Path.explode(s) + val node = append(master.master_dir, Resources.thy_path(path)) + val master_dir = append(master.master_dir, path.dir) + Document.Node.Name(node, master_dir, theory) + } + } + + def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = + { + try { + val header = Thy_Header.read(text) + + val name1 = header.name + if (name.theory != name1) + error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) + + " for theory " + quote(name1)) + + val imports = header.imports.map(import_name(name, _)) + Document.Node.Header(imports, header.keywords, Nil) + } + catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } + } + + def check_thy(name: Document.Node.Name): Document.Node.Header = + with_thy_text(name, check_thy_text(name, _)) + + + /* theory text edits */ + + def text_edits( + reparse_limit: Int, + previous: Document.Version, + doc_blobs: Document.Blobs, + edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) = + Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits) + + def syntax_changed() { } +} + diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/ROOT --- a/src/Pure/ROOT Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/ROOT Tue Mar 18 17:39:03 2014 +0100 @@ -161,6 +161,7 @@ "PIDE/markup.ML" "PIDE/protocol.ML" "PIDE/query_operation.ML" + "PIDE/resources.ML" "PIDE/xml.ML" "PIDE/yxml.ML" "Proof/extraction.ML" @@ -198,7 +199,6 @@ "Thy/thm_deps.ML" "Thy/thy_header.ML" "Thy/thy_info.ML" - "Thy/thy_load.ML" "Thy/thy_output.ML" "Thy/thy_syntax.ML" "Tools/build.ML" diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 18 17:39:03 2014 +0100 @@ -281,7 +281,7 @@ use "Thy/present.ML"; use "PIDE/command.ML"; use "PIDE/query_operation.ML"; -use "Thy/thy_load.ML"; +use "PIDE/resources.ML"; use "Thy/thy_info.ML"; use "PIDE/document.ML"; diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/System/session.scala Tue Mar 18 17:39:03 2014 +0100 @@ -109,7 +109,7 @@ } -class Session(val thy_load: Thy_Load) +class Session(val resources: Resources) { /* global flags */ @@ -180,8 +180,8 @@ case Text_Edits(previous, doc_blobs, text_edits, version_result) => val prev = previous.get_finished val (syntax_changed, doc_edits, version) = - Timing.timeit("Thy_Load.text_edits", timing) { - thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits) + Timing.timeit("text_edits", timing) { + resources.text_edits(reparse_limit, prev, doc_blobs, text_edits) } version_result.fulfill(version) sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version) @@ -216,7 +216,7 @@ def recent_syntax(): Outer_Syntax = { val version = current_state().recent_finished.version.get_finished - if (version.is_init) thy_load.base_syntax + if (version.is_init) resources.base_syntax else version.syntax } @@ -238,7 +238,7 @@ def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text = { val header1 = - if (thy_load.loaded_theories(name.theory)) + if (resources.loaded_theories(name.theory)) header.error("Cannot update finished theory " + quote(name.theory)) else header (name, Document.Node.Deps(header1)) @@ -401,7 +401,7 @@ global_state >> (_.define_version(version, assignment)) prover.get.update(previous.id, version.id, doc_edits) - if (syntax_changed) thy_load.syntax_changed() + if (syntax_changed) resources.syntax_changed() } //}}} diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Mar 18 17:39:03 2014 +0100 @@ -123,13 +123,13 @@ SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); -val get_imports = Thy_Load.imports_of o get_theory; +val get_imports = Resources.imports_of o get_theory; (*Proof General legacy*) fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () => (case get_deps name of NONE => [] - | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name))); + | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name))); @@ -284,7 +284,7 @@ val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = - Thy_Load.load_thy document last_timing update_time dir header text_pos text + Resources.load_thy document last_timing update_time dir header text_pos text (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); fun commit () = update_thy deps theory; in @@ -295,18 +295,18 @@ (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => - let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name + let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', - keywords = keywords'} = Thy_Load.check_thy dir name; + keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false - | SOME theory => Thy_Load.loaded_files_current theory); + | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in @@ -317,7 +317,7 @@ let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); - val node_name = File.full_path dir (Thy_Load.thy_path path); + val node_name = File.full_path dir (Resources.thy_path path); fun check_entry (Task (node_name', _, _)) = if node_name = node_name' then () else @@ -384,7 +384,7 @@ val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports; val _ = Thy_Header.define_keywords header; val parents = map (get_theory o base_name o fst) imports; - in Thy_Load.begin_theory master_dir header parents end; + in Resources.begin_theory master_dir header parents end; (* register theory *) @@ -392,8 +392,8 @@ fun register_thy theory = let val name = Context.theory_name theory; - val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; - val imports = Thy_Load.imports_of theory; + val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; + val imports = Resources.imports_of theory; in NAMED_CRITICAL "Thy_Info" (fn () => (kill_thy name; diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Thy/thy_info.scala Tue Mar 18 17:39:03 2014 +0100 @@ -10,7 +10,7 @@ import java.util.concurrent.{Future => JFuture} -class Thy_Info(thy_load: Thy_Load) +class Thy_Info(resources: Resources) { /* messages */ @@ -33,9 +33,9 @@ { def load_files(syntax: Outer_Syntax): List[String] = { - val string = thy_load.with_thy_text(name, _.toString) - if (thy_load.body_files_test(syntax, string)) - thy_load.body_files(syntax, string) + val string = resources.with_thy_text(name, _.toString) + if (resources.body_files_test(syntax, string)) + resources.body_files(syntax, string) else Nil } } @@ -71,7 +71,7 @@ val import_errors = (for { (theory, names) <- seen_names.iterator_list - if !thy_load.loaded_theories(theory) + if !resources.loaded_theories(theory) if names.length > 1 } yield "Incoherent imports for theory " + quote(theory) + ":\n" + @@ -82,10 +82,10 @@ header_errors ::: import_errors } - lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) + lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords) def loaded_theories: Set[String] = - (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } + (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } def load_files: List[Path] = { @@ -115,13 +115,13 @@ required_by(initiators) + Position.here(require_pos) val required1 = required + thy - if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory)) + if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory)) required1 else { try { if (initiators.contains(name)) error(cycle_msg(initiators)) val header = - try { thy_load.check_thy(name).cat_errors(message) } + try { resources.check_thy(name).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } val imports = header.imports.map((_, Position.File(name.node))) Dep(name, header) :: require_thys(name :: initiators, required1, imports) diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Tue Mar 18 16:45:14 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,243 +0,0 @@ -(* Title: Pure/Thy/thy_load.ML - Author: Makarius - -Management of theory sources and auxiliary files. -*) - -signature THY_LOAD = -sig - val master_directory: theory -> Path.T - val imports_of: theory -> (string * Position.T) list - val thy_path: Path.T -> Path.T - 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 parse_files: string -> (theory -> Token.file list) parser - val provide: Path.T * SHA1.digest -> theory -> theory - val provide_parse_files: string -> (theory -> Token.file list * theory) parser - val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string - val loaded_files: theory -> Path.T list - val loaded_files_current: theory -> bool - val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory - val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> - Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int -end; - -structure Thy_Load: THY_LOAD = -struct - -(* manage source files *) - -type files = - {master_dir: Path.T, (*master directory of theory source*) - imports: (string * Position.T) list, (*source specification of imports*) - provided: (Path.T * SHA1.digest) list}; (*source path, digest*) - -fun make_files (master_dir, imports, provided): files = - {master_dir = master_dir, imports = imports, provided = provided}; - -structure Files = Theory_Data -( - type T = files; - val empty = make_files (Path.current, [], []); - fun extend _ = empty; - fun merge _ = empty; -); - -fun map_files f = - Files.map (fn {master_dir, imports, provided} => - make_files (f (master_dir, imports, provided))); - - -val master_directory = #master_dir o Files.get; -val imports_of = #imports o Files.get; - -fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, [])); - - -(* theory files *) - -val thy_path = Path.ext "thy"; - -fun check_file dir file = File.check_file (File.full_path dir file); - -fun check_thy dir thy_name = - let - val path = thy_path (Path.basic thy_name); - val master_file = check_file dir path; - val text = File.read master_file; - - val {name = (name, pos), imports, keywords} = - Thy_Header.read (Path.position master_file) text; - val _ = thy_name <> name andalso - error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos); - in - {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, - imports = imports, keywords = keywords} - end; - - -(* load files *) - -fun parse_files cmd = - Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => - (case Token.get_files tok of - [] => - let - val master_dir = master_directory thy; - val pos = Token.pos_of tok; - val src_paths = Keyword.command_files cmd (Path.explode name); - in map (Command.read_file master_dir pos) src_paths end - | files => map Exn.release files)); - -fun provide (src_path, id) = - map_files (fn (master_dir, imports, provided) => - if AList.defined (op =) provided src_path then - error ("Duplicate use of source file: " ^ Path.print src_path) - else (master_dir, imports, (src_path, id) :: provided)); - -fun provide_parse_files cmd = - parse_files cmd >> (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); - -fun load_file thy src_path = - let - val full_path = check_file (master_directory thy) src_path; - val text = File.read full_path; - val id = SHA1.digest text; - in ((full_path, id), text) end; - -fun loaded_files_current thy = - #provided (Files.get thy) |> - forall (fn (src_path, id) => - (case try (load_file thy) src_path of - NONE => false - | SOME ((_, id'), _) => id = id')); - -(*Proof General legacy*) -fun loaded_files thy = - let val {master_dir, provided, ...} = Files.get thy - in map (File.full_path master_dir o #1) provided end; - - -(* load theory *) - -fun begin_theory master_dir {name, imports, keywords} parents = - Theory.begin_theory name parents - |> put_deps master_dir imports - |> fold Thy_Header.declare_keyword keywords; - -fun excursion master_dir last_timing init elements = - let - fun prepare_span span = - Thy_Syntax.span_content span - |> Command.read init master_dir [] - |> (fn tr => Toplevel.put_timing (last_timing tr) tr); - - fun element_result span_elem (st, _) = - let - val elem = Thy_Syntax.map_element prepare_span span_elem; - val (results, st') = Toplevel.element_result elem st; - val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); - in (results, (st', pos')) end; - - val (results, (end_state, end_pos)) = - fold_map element_result elements (Toplevel.toplevel, Position.none); - - val thy = Toplevel.end_theory end_pos end_state; - in (results, thy) end; - -fun load_thy document last_timing update_time master_dir header text_pos text parents = - let - val time = ! Toplevel.timing; - - val {name = (name, _), ...} = header; - val _ = Thy_Header.define_keywords header; - - val lexs = Keyword.get_lexicons (); - val toks = Thy_Syntax.parse_tokens lexs text_pos text; - val spans = Thy_Syntax.parse_spans toks; - val elements = Thy_Syntax.parse_elements spans; - - fun init () = - begin_theory master_dir header parents - |> Present.begin_theory update_time - (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); - - val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); - val (results, thy) = - cond_timeit time "" (fn () => excursion master_dir last_timing init elements); - val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); - - fun present () = - let - val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results); - val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); - in - if exists (Toplevel.is_skipped_proof o #2) res then - warning ("Cannot present theory with skipped proofs: " ^ quote name) - else - let val tex_source = - Thy_Output.present_thy minor Keyword.command_tags - (Outer_Syntax.is_markup outer_syntax) res toks - |> Buffer.content; - in if document then Present.theory_output name tex_source else () end - end; - - in (thy, present, size text) end; - - -(* antiquotations *) - -local - -fun check_path strict ctxt dir (name, pos) = - let - val _ = Context_Position.report ctxt pos Markup.language_path; - - val path = Path.append dir (Path.explode name) - handle ERROR msg => error (msg ^ Position.here pos); - - val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); - val _ = - if can Path.expand path andalso File.exists path then () - else - let - val path' = perhaps (try Path.expand) path; - val msg = "Bad file: " ^ Path.print path' ^ Position.here pos; - in - if strict then error msg - else - Context_Position.if_visible ctxt Output.report - (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg) - end; - in path end; - -fun file_antiq strict ctxt (name, pos) = - let - val dir = master_directory (Proof_Context.theory_of ctxt); - val _ = check_path strict ctxt dir (name, pos); - in - space_explode "/" name - |> map Thy_Output.verb_text - |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}") - end; - -in - -val _ = Theory.setup - (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path)) - (file_antiq true o #context) #> - Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path)) - (file_antiq false o #context) #> - ML_Antiquotation.value @{binding path} - (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) => - let val path = check_path true ctxt Path.current arg - in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end))); - -end; - -end; diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Tue Mar 18 16:45:14 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,111 +0,0 @@ -/* Title: Pure/Thy/thy_load.scala - Author: Makarius - -Primitives for loading theory files. -*/ - -package isabelle - - -import scala.annotation.tailrec - -import java.io.{File => JFile} - - -object Thy_Load -{ - /* paths */ - - def thy_path(path: Path): Path = path.ext("thy") - - def is_wellformed(str: String): Boolean = - try { thy_path(Path.explode(str)); true } - catch { case ERROR(_) => false } -} - - -class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax) -{ - /* document node names */ - - def node_name(raw_path: Path): Document.Node.Name = - { - val path = raw_path.expand - val node = path.implode - val theory = Thy_Header.thy_name(node).getOrElse("") - val master_dir = if (theory == "") "" else path.dir.implode - Document.Node.Name(node, master_dir, theory) - } - - - /* file-system operations */ - - def append(dir: String, source_path: Path): String = - (Path.explode(dir) + source_path).expand.implode - - def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = - { - val path = Path.explode(name.node) - if (!path.is_file) error("No such file: " + path.toString) - - val text = File.read(path) - Symbol.decode_strict(text) - f(text) - } - - - /* theory files */ - - def body_files_test(syntax: Outer_Syntax, text: String): Boolean = - syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) - - def body_files(syntax: Outer_Syntax, text: String): List[String] = - { - val spans = Thy_Syntax.parse_spans(syntax.scan(text)) - spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList - } - - def import_name(master: Document.Node.Name, s: String): Document.Node.Name = - { - val theory = Thy_Header.base_name(s) - if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory) - else { - val path = Path.explode(s) - val node = append(master.master_dir, Thy_Load.thy_path(path)) - val master_dir = append(master.master_dir, path.dir) - Document.Node.Name(node, master_dir, theory) - } - } - - def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = - { - try { - val header = Thy_Header.read(text) - - val name1 = header.name - if (name.theory != name1) - error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + - " for theory " + quote(name1)) - - val imports = header.imports.map(import_name(name, _)) - Document.Node.Header(imports, header.keywords, Nil) - } - catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } - } - - def check_thy(name: Document.Node.Name): Document.Node.Header = - with_thy_text(name, check_thy_text(name, _)) - - - /* theory text edits */ - - def text_edits( - reparse_limit: Int, - previous: Document.Version, - doc_blobs: Document.Blobs, - edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) = - Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits) - - def syntax_changed() { } -} - diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Tue Mar 18 17:39:03 2014 +0100 @@ -257,7 +257,7 @@ } def resolve_files( - thy_load: Thy_Load, + resources: Resources, syntax: Outer_Syntax, node_name: Document.Node.Name, span: List[Token], @@ -267,7 +267,7 @@ span_files(syntax, span).map(file_name => Exn.capture { val name = - Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name))) + Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) (name, blob) }) @@ -289,7 +289,7 @@ } private def reparse_spans( - thy_load: Thy_Load, + resources: Resources, syntax: Outer_Syntax, doc_blobs: Document.Blobs, name: Document.Node.Name, @@ -299,7 +299,7 @@ val cmds0 = commands.iterator(first, last).toList val blobs_spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). - map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span)) + map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span)) val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0) @@ -324,7 +324,7 @@ // FIXME somewhat slow private def recover_spans( - thy_load: Thy_Load, + resources: Resources, syntax: Outer_Syntax, doc_blobs: Document.Blobs, name: Document.Node.Name, @@ -342,7 +342,7 @@ case Some(first_unparsed) => val first = next_invisible_command(cmds.reverse, first_unparsed) val last = next_invisible_command(cmds, first_unparsed) - recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last)) + recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last)) case None => cmds } recover(commands) @@ -352,7 +352,7 @@ /* consolidate unfinished spans */ private def consolidate_spans( - thy_load: Thy_Load, + resources: Resources, syntax: Outer_Syntax, doc_blobs: Document.Blobs, reparse_limit: Int, @@ -374,7 +374,7 @@ last = it.next i += last.length } - reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last) + reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last) case None => commands } case None => commands @@ -396,7 +396,7 @@ } private def text_edit( - thy_load: Thy_Load, + resources: Resources, syntax: Outer_Syntax, doc_blobs: Document.Blobs, reparse_limit: Int, @@ -413,7 +413,7 @@ val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) val commands2 = - recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) + recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1) node.update_commands(commands2) } @@ -426,13 +426,13 @@ if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit, + consolidate_spans(resources, syntax, doc_blobs, reparse_limit, name, visible, node.commands)) } } def text_edits( - thy_load: Thy_Load, + resources: Resources, reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, @@ -440,7 +440,7 @@ : (Boolean, List[Document.Edit_Command], Document.Version) = { val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) = - header_edits(thy_load.base_syntax, previous, edits) + header_edits(resources.base_syntax, previous, edits) if (edits.isEmpty) (false, Nil, Document.Version.make(syntax, previous.nodes)) @@ -469,10 +469,10 @@ val node1 = if (reparse_set(name) && !commands.isEmpty) node.update_commands( - reparse_spans(thy_load, syntax, doc_blobs, + reparse_spans(resources, syntax, doc_blobs, name, commands, commands.head, commands.last)) else node - val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _)) + val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) if (!(node.same_perspective(node2.perspective))) doc_edits += (name -> node2.perspective) diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Tools/build.scala Tue Mar 18 17:39:03 2014 +0100 @@ -419,8 +419,8 @@ val parent = deps(parent_name) (parent.loaded_theories, parent.syntax) } - val thy_load = new Thy_Load(preloaded, parent_syntax) - val thy_info = new Thy_Info(thy_load) + val resources = new Resources(preloaded, parent_syntax) + val thy_info = new Thy_Info(resources) if (verbose || list_files) { val groups = @@ -432,7 +432,7 @@ val thy_deps = thy_info.dependencies( info.theories.map(_._2).flatten. - map(thy => (thy_load.node_name(info.dir + Thy_Load.thy_path(thy)), info.pos))) + map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos))) thy_deps.errors match { case Nil => diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/Tools/proof_general.ML Tue Mar 18 17:39:03 2014 +0100 @@ -337,7 +337,7 @@ Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ())) handle ERROR msg => (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); - tell_file_retracted (Thy_Load.thy_path (Path.basic name))) + tell_file_retracted (Resources.thy_path (Path.basic name))) val _ = Isar.init (); in () end; diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/build-jars --- a/src/Pure/build-jars Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/build-jars Tue Mar 18 17:39:03 2014 +0100 @@ -53,6 +53,7 @@ PIDE/markup_tree.scala PIDE/protocol.scala PIDE/query_operation.scala + PIDE/resources.scala PIDE/text.scala PIDE/xml.scala PIDE/yxml.scala @@ -73,7 +74,6 @@ Thy/present.scala Thy/thy_header.scala Thy/thy_info.scala - Thy/thy_load.scala Thy/thy_syntax.scala Tools/build.scala Tools/doc.scala diff -r 52d5067ca06a -r 06cc31dff138 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/pure_syn.ML Tue Mar 18 17:39:03 2014 +0100 @@ -18,10 +18,10 @@ val _ = Outer_Syntax.command (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" - (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => + (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => let val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); - val provide = Thy_Load.provide (src_path, digest); + val provide = Resources.provide (src_path, digest); val source = {delimited = true, text = cat_lines lines, pos = pos}; in gthy diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Tue Mar 18 17:39:03 2014 +0100 @@ -325,7 +325,7 @@ let val preamble = "(* Generated from " ^ - Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^ + Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ "; DO NOT EDIT! *)"; val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); in diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/Code/code_target.ML Tue Mar 18 17:39:03 2014 +0100 @@ -380,7 +380,8 @@ | assert_module_name module_name = module_name; fun using_master_directory ctxt = - Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt))); + Option.map (Path.append (File.pwd ()) o + Path.append (Resources.master_directory (Proof_Context.theory_of ctxt))); in diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 17:39:03 2014 +0100 @@ -27,7 +27,7 @@ "src/jedit_editor.scala" "src/jedit_lib.scala" "src/jedit_options.scala" - "src/jedit_thy_load.scala" + "src/jedit_resources.scala" "src/monitor_dockable.scala" "src/output_dockable.scala" "src/plugin.scala" diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 18 17:39:03 2014 +0100 @@ -70,7 +70,7 @@ if (is_theory) { JEdit_Lib.buffer_lock(buffer) { Exn.capture { - PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) + PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) } match { case Exn.Res(header) => header case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) @@ -150,7 +150,7 @@ _blob match { case Some(x) => x case None => - val bytes = PIDE.thy_load.file_content(buffer) + val bytes = PIDE.resources.file_content(buffer) val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength)) _blob = Some((bytes, file)) (bytes, file) diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/find_dockable.scala Tue Mar 18 17:39:03 2014 +0100 @@ -131,7 +131,7 @@ private val context_entries = new Context_Entry("", "current context") :: - PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name)) + PIDE.resources.loaded_theories.toList.sorted.map(name => Context_Entry(name, name)) private val context = new ComboBox[Context_Entry](context_entries) { tooltip = "Search in pre-loaded theory (default: context of current command)" diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Mar 18 17:39:03 2014 +0100 @@ -133,7 +133,7 @@ class Isabelle_Sidekick_Default extends - Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name) + Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name) class Isabelle_Sidekick_Options extends diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/jedit_resources.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Mar 18 17:39:03 2014 +0100 @@ -0,0 +1,123 @@ +/* Title: Tools/jEdit/src/jedit_resources.scala + Author: Makarius + +Resources for theories and auxiliary files, based on jEdit buffer +content and virtual file-systems. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.io.{File => JFile, IOException, ByteArrayOutputStream} +import javax.swing.text.Segment + +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} +import org.gjt.sp.jedit.MiscUtilities +import org.gjt.sp.jedit.{jEdit, View, Buffer} +import org.gjt.sp.jedit.bufferio.BufferIORequest + + +class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) + extends Resources(loaded_theories, base_syntax) +{ + /* document node names */ + + def node_name(buffer: Buffer): Document.Node.Name = + { + val node = JEdit_Lib.buffer_name(buffer) + val theory = Thy_Header.thy_name(node).getOrElse("") + val master_dir = if (theory == "") "" else buffer.getDirectory + Document.Node.Name(node, master_dir, theory) + } + + def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = + { + val name = node_name(buffer) + if (name.is_theory) Some(name) else None + } + + + /* file-system operations */ + + override def append(dir: String, source_path: Path): String = + { + val path = source_path.expand + if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path) + else { + val vfs = VFSManager.getVFSForPath(dir) + if (vfs.isInstanceOf[FileVFS]) + MiscUtilities.resolveSymlinks( + vfs.constructPath(dir, Isabelle_System.platform_path(path))) + else vfs.constructPath(dir, Isabelle_System.standard_path(path)) + } + } + + override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = + { + Swing_Thread.now { + JEdit_Lib.jedit_buffer(name.node) match { + case Some(buffer) => + JEdit_Lib.buffer_lock(buffer) { + Some(f(buffer.getSegment(0, buffer.getLength))) + } + case None => None + } + } getOrElse { + val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) + f(File.read(file)) + } + } + + def check_file(view: View, path: String): Boolean = + { + val vfs = VFSManager.getVFSForPath(path) + val session = vfs.createVFSSession(path, view) + + try { + session != null && { + try { + val file = vfs._getFile(session, path, view) + file != null && file.isReadable && file.getType == VFSFile.FILE + } + catch { case _: IOException => false } + } + } + finally { + try { vfs._endVFSSession(session, view) } + catch { case _: IOException => } + } + } + + + /* file content */ + + def file_content(buffer: Buffer): Bytes = + { + val path = buffer.getPath + val vfs = VFSManager.getVFSForPath(path) + val content = + new BufferIORequest(null, buffer, null, vfs, path) { + def _run() { } + def apply(): Bytes = + { + val out = + new ByteArrayOutputStream(buffer.getLength + 1) { + def content(): Bytes = Bytes(this.buf, 0, this.count) + } + write(buffer, out) + out.content() + } + } + content() + } + + + /* theory text edits */ + + override def syntax_changed(): Unit = + Swing_Thread.later { jEdit.propertiesChanged() } +} + diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/jedit_thy_load.scala --- a/src/Tools/jEdit/src/jedit_thy_load.scala Tue Mar 18 16:45:14 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ -/* Title: Tools/jEdit/src/jedit_thy_load.scala - Author: Makarius - -Primitives for loading theory files, based on jEdit buffer content. -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.io.{File => JFile, IOException, ByteArrayOutputStream} -import javax.swing.text.Segment - -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} -import org.gjt.sp.jedit.MiscUtilities -import org.gjt.sp.jedit.{jEdit, View, Buffer} -import org.gjt.sp.jedit.bufferio.BufferIORequest - -class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) - extends Thy_Load(loaded_theories, base_syntax) -{ - /* document node names */ - - def node_name(buffer: Buffer): Document.Node.Name = - { - val node = JEdit_Lib.buffer_name(buffer) - val theory = Thy_Header.thy_name(node).getOrElse("") - val master_dir = if (theory == "") "" else buffer.getDirectory - Document.Node.Name(node, master_dir, theory) - } - - def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = - { - val name = node_name(buffer) - if (name.is_theory) Some(name) else None - } - - - /* file-system operations */ - - override def append(dir: String, source_path: Path): String = - { - val path = source_path.expand - if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path) - else { - val vfs = VFSManager.getVFSForPath(dir) - if (vfs.isInstanceOf[FileVFS]) - MiscUtilities.resolveSymlinks( - vfs.constructPath(dir, Isabelle_System.platform_path(path))) - else vfs.constructPath(dir, Isabelle_System.standard_path(path)) - } - } - - override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = - { - Swing_Thread.now { - JEdit_Lib.jedit_buffer(name.node) match { - case Some(buffer) => - JEdit_Lib.buffer_lock(buffer) { - Some(f(buffer.getSegment(0, buffer.getLength))) - } - case None => None - } - } getOrElse { - val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) - if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) - f(File.read(file)) - } - } - - def check_file(view: View, path: String): Boolean = - { - val vfs = VFSManager.getVFSForPath(path) - val session = vfs.createVFSSession(path, view) - - try { - session != null && { - try { - val file = vfs._getFile(session, path, view) - file != null && file.isReadable && file.getType == VFSFile.FILE - } - catch { case _: IOException => false } - } - } - finally { - try { vfs._endVFSSession(session, view) } - catch { case _: IOException => } - } - } - - - /* file content */ - - def file_content(buffer: Buffer): Bytes = - { - val path = buffer.getPath - val vfs = VFSManager.getVFSForPath(path) - val content = - new BufferIORequest(null, buffer, null, vfs, path) { - def _run() { } - def apply(): Bytes = - { - val out = - new ByteArrayOutputStream(buffer.getLength + 1) { - def content(): Bytes = Bytes(this.buf, 0, this.count) - } - write(buffer, out) - out.content() - } - } - content() - } - - - /* theory text edits */ - - override def syntax_changed(): Unit = - Swing_Thread.later { jEdit.propertiesChanged() } -} - diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 18 17:39:03 2014 +0100 @@ -36,12 +36,12 @@ @volatile var startup_notified = false @volatile var plugin: Plugin = null - @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty)) + @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty)) def options_changed() { plugin.options_changed() } - def thy_load(): JEdit_Thy_Load = - session.thy_load.asInstanceOf[JEdit_Thy_Load] + def resources(): JEdit_Resources = + session.resources.asInstanceOf[JEdit_Resources] lazy val editor = new JEdit_Editor @@ -109,7 +109,7 @@ if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED) } { JEdit_Lib.buffer_lock(buffer) { - val node_name = thy_load.node_name(buffer) + val node_name = resources.node_name(buffer) val model = document_model(buffer) match { case Some(model) if model.node_name == node_name => model @@ -202,10 +202,10 @@ if model.is_theory } yield (model.node_name, Position.none) - val thy_info = new Thy_Info(PIDE.thy_load) + val thy_info = new Thy_Info(PIDE.resources) // FIXME avoid I/O in Swing thread!?! val files = thy_info.dependencies(thys).deps.map(_.name.node). - filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file)) + filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) if (!files.isEmpty) { if (PIDE.options.bool("jedit_auto_load")) { @@ -349,9 +349,9 @@ JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) val content = Isabelle_Logic.session_content(false) - val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) + val resources = new JEdit_Resources(content.loaded_theories, content.syntax) - PIDE.session = new Session(thy_load) { + PIDE.session = new Session(resources) { override def output_delay = PIDE.options.seconds("editor_output_delay") override def reparse_limit = PIDE.options.int("editor_reparse_limit") } diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Mar 18 17:39:03 2014 +0100 @@ -336,7 +336,7 @@ { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) if Path.is_valid(name) => - val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name)) + val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name)) val link = PIDE.editor.hyperlink_file(jedit_file) Some(links :+ Text.Info(snapshot.convert(info_range), link)) @@ -470,7 +470,7 @@ Some(add(prev, r, (true, XML.Text(txt1 + txt2)))) case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) if Path.is_valid(name) => - val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name)) + val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name)) val text = "path " + quote(name) + "\nfile " + quote(jedit_file) Some(add(prev, r, (true, XML.Text(text)))) case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 18 17:39:03 2014 +0100 @@ -192,7 +192,7 @@ }).filter(_._1.is_theory) val nodes_status1 = (nodes_status /: iterator)({ case (status, (name, node)) => - if (PIDE.thy_load.loaded_theories(name.theory)) status + if (PIDE.resources.loaded_theories(name.theory)) status else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) if (nodes_status != nodes_status1) { diff -r 52d5067ca06a -r 06cc31dff138 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 18 17:39:03 2014 +0100 @@ -186,7 +186,7 @@ } val nodes_timing1 = (nodes_timing /: iterator)({ case (timing1, (name, node)) => - if (PIDE.thy_load.loaded_theories(name.theory)) timing1 + if (PIDE.resources.loaded_theories(name.theory)) timing1 else { val node_timing = Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)