clarifed module name;
authorwenzelm
Tue Mar 18 17:39:03 2014 +0100 (2014-03-18)
changeset 5620806cc31dff138
parent 56207 52d5067ca06a
child 56209 3c89e21d9be2
clarifed module name;
src/Doc/Codegen/Setup.thy
src/Doc/Tutorial/ToyList/ToyList_Test.thy
src/Doc/antiquote_setup.ML
src/HOL/SMT_Examples/boogie.ML
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT2/smt2_config.ML
src/Pure/Isar/parse.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/proof_general.ML
src/Pure/build-jars
src/Pure/pure_syn.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Doc/Codegen/Setup.thy	Tue Mar 18 16:45:14 2014 +0100
     1.2 +++ b/src/Doc/Codegen/Setup.thy	Tue Mar 18 17:39:03 2014 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  (* FIXME avoid writing into source directory *)
     1.6  ML {*
     1.7 -  Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples"))
     1.8 +  Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples"))
     1.9  *}
    1.10  
    1.11  ML_file "../antiquote_setup.ML"
     2.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Tue Mar 18 16:45:14 2014 +0100
     2.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Tue Mar 18 17:39:03 2014 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  ML {*  (* FIXME somewhat non-standard, fragile *)
     2.5    let
     2.6      val texts =
     2.7 -      map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
     2.8 +      map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
     2.9          ["ToyList1", "ToyList2"];
    2.10      val trs = Outer_Syntax.parse Position.start (implode texts);
    2.11      val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
     3.1 --- a/src/Doc/antiquote_setup.ML	Tue Mar 18 16:45:14 2014 +0100
     3.2 +++ b/src/Doc/antiquote_setup.ML	Tue Mar 18 17:39:03 2014 +0100
     3.3 @@ -152,7 +152,7 @@
     3.4  val _ =
     3.5    Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
     3.6      (fn {context = ctxt, ...} =>
     3.7 -      fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
     3.8 +      fn name => (Resources.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
     3.9  
    3.10  
    3.11  (* Isabelle/jEdit elements *)
     4.1 --- a/src/HOL/SMT_Examples/boogie.ML	Tue Mar 18 16:45:14 2014 +0100
     4.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Tue Mar 18 17:39:03 2014 +0100
     4.3 @@ -317,7 +317,7 @@
     4.4  val _ =
     4.5    Outer_Syntax.command @{command_spec "boogie_file"}
     4.6      "prove verification condition from .b2i file"
     4.7 -    (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
     4.8 +    (Resources.provide_parse_files "boogie_file" >> (fn files =>
     4.9        Toplevel.theory (fn thy =>
    4.10          let
    4.11            val ([{lines, ...}], thy') = files thy;
     5.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Tue Mar 18 16:45:14 2014 +0100
     5.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Mar 18 17:39:03 2014 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4      val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
     5.5        {lines = fdl_lines, pos = fdl_pos, ...},
     5.6        {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
     5.7 -    val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path));
     5.8 +    val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
     5.9    in
    5.10      SPARK_VCs.set_vcs
    5.11        (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
    5.12 @@ -24,7 +24,7 @@
    5.13  (* FIXME *)
    5.14  fun spark_open_old (vc_name, prfx) thy =
    5.15    let
    5.16 -    val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
    5.17 +    val ((vc_path, vc_id), vc_text) = Resources.load_file thy (Path.explode vc_name);
    5.18      val (base, header) =
    5.19        (case Path.split_ext vc_path of
    5.20          (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
    5.21 @@ -117,13 +117,13 @@
    5.22  val _ =
    5.23    Outer_Syntax.command @{command_spec "spark_open_vcg"}
    5.24      "open a new SPARK environment and load a SPARK-generated .vcg file"
    5.25 -    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_vcg"
    5.26 +    (Parse.parname -- Resources.provide_parse_files "spark_open_vcg"
    5.27        >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
    5.28  
    5.29  val _ =
    5.30    Outer_Syntax.command @{command_spec "spark_open_siv"}
    5.31      "open a new SPARK environment and load a SPARK-generated .siv file"
    5.32 -    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_siv"
    5.33 +    (Parse.parname -- Resources.provide_parse_files "spark_open_siv"
    5.34        >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
    5.35  
    5.36  val pfun_type = Scan.option
     6.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Mar 18 16:45:14 2014 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Mar 18 17:39:03 2014 +0100
     6.3 @@ -198,7 +198,7 @@
     6.4    if name = "" then NONE
     6.5    else
     6.6      Path.explode name
     6.7 -    |> Path.append (Thy_Load.master_directory (Context.theory_of context))
     6.8 +    |> Path.append (Resources.master_directory (Context.theory_of context))
     6.9      |> SOME o Cache_IO.unsynchronized_init)
    6.10  
    6.11  val certificates_of = Certificates.get o Context.Proof
     7.1 --- a/src/HOL/Tools/SMT2/smt2_config.ML	Tue Mar 18 16:45:14 2014 +0100
     7.2 +++ b/src/HOL/Tools/SMT2/smt2_config.ML	Tue Mar 18 17:39:03 2014 +0100
     7.3 @@ -195,7 +195,7 @@
     7.4    if name = "" then NONE
     7.5    else
     7.6      Path.explode name
     7.7 -    |> Path.append (Thy_Load.master_directory (Context.theory_of context))
     7.8 +    |> Path.append (Resources.master_directory (Context.theory_of context))
     7.9      |> SOME o Cache_IO.unsynchronized_init)
    7.10  
    7.11  val certificates_of = Certificates.get o Context.Proof
     8.1 --- a/src/Pure/Isar/parse.scala	Tue Mar 18 16:45:14 2014 +0100
     8.2 +++ b/src/Pure/Isar/parse.scala	Tue Mar 18 17:39:03 2014 +0100
     8.3 @@ -64,7 +64,7 @@
     8.4      def path: Parser[String] =
     8.5        atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     8.6      def theory_name: Parser[String] =
     8.7 -      atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content))
     8.8 +      atom("theory name", tok => tok.is_name && Resources.is_wellformed_thy_path(tok.content))
     8.9  
    8.10      private def tag_name: Parser[String] =
    8.11        atom("tag name", tok =>
     9.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 18 16:45:14 2014 +0100
     9.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 18 17:39:03 2014 +0100
     9.3 @@ -443,7 +443,7 @@
     9.4                  NONE => Toplevel.toplevel
     9.5                | SOME eval => Command.eval_result_state eval)));
     9.6      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
     9.7 -  in Thy_Load.begin_theory master_dir header parents end;
     9.8 +  in Resources.begin_theory master_dir header parents end;
     9.9  
    9.10  fun check_theory full name node =
    9.11    is_some (loaded_theory name) orelse
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/PIDE/resources.ML	Tue Mar 18 17:39:03 2014 +0100
    10.3 @@ -0,0 +1,243 @@
    10.4 +(*  Title:      Pure/PIDE/resources.ML
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Resources for theories and auxiliary files.
    10.8 +*)
    10.9 +
   10.10 +signature RESOURCES =
   10.11 +sig
   10.12 +  val master_directory: theory -> Path.T
   10.13 +  val imports_of: theory -> (string * Position.T) list
   10.14 +  val thy_path: Path.T -> Path.T
   10.15 +  val check_thy: Path.T -> string ->
   10.16 +   {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
   10.17 +    imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   10.18 +  val parse_files: string -> (theory -> Token.file list) parser
   10.19 +  val provide: Path.T * SHA1.digest -> theory -> theory
   10.20 +  val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   10.21 +  val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   10.22 +  val loaded_files: theory -> Path.T list
   10.23 +  val loaded_files_current: theory -> bool
   10.24 +  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   10.25 +  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
   10.26 +    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
   10.27 +end;
   10.28 +
   10.29 +structure Resources: RESOURCES =
   10.30 +struct
   10.31 +
   10.32 +(* manage source files *)
   10.33 +
   10.34 +type files =
   10.35 + {master_dir: Path.T,  (*master directory of theory source*)
   10.36 +  imports: (string * Position.T) list,  (*source specification of imports*)
   10.37 +  provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
   10.38 +
   10.39 +fun make_files (master_dir, imports, provided): files =
   10.40 + {master_dir = master_dir, imports = imports, provided = provided};
   10.41 +
   10.42 +structure Files = Theory_Data
   10.43 +(
   10.44 +  type T = files;
   10.45 +  val empty = make_files (Path.current, [], []);
   10.46 +  fun extend _ = empty;
   10.47 +  fun merge _ = empty;
   10.48 +);
   10.49 +
   10.50 +fun map_files f =
   10.51 +  Files.map (fn {master_dir, imports, provided} =>
   10.52 +    make_files (f (master_dir, imports, provided)));
   10.53 +
   10.54 +
   10.55 +val master_directory = #master_dir o Files.get;
   10.56 +val imports_of = #imports o Files.get;
   10.57 +
   10.58 +fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
   10.59 +
   10.60 +
   10.61 +(* theory files *)
   10.62 +
   10.63 +val thy_path = Path.ext "thy";
   10.64 +
   10.65 +fun check_file dir file = File.check_file (File.full_path dir file);
   10.66 +
   10.67 +fun check_thy dir thy_name =
   10.68 +  let
   10.69 +    val path = thy_path (Path.basic thy_name);
   10.70 +    val master_file = check_file dir path;
   10.71 +    val text = File.read master_file;
   10.72 +
   10.73 +    val {name = (name, pos), imports, keywords} =
   10.74 +      Thy_Header.read (Path.position master_file) text;
   10.75 +    val _ = thy_name <> name andalso
   10.76 +      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
   10.77 +  in
   10.78 +   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
   10.79 +    imports = imports, keywords = keywords}
   10.80 +  end;
   10.81 +
   10.82 +
   10.83 +(* load files *)
   10.84 +
   10.85 +fun parse_files cmd =
   10.86 +  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
   10.87 +    (case Token.get_files tok of
   10.88 +      [] =>
   10.89 +        let
   10.90 +          val master_dir = master_directory thy;
   10.91 +          val pos = Token.pos_of tok;
   10.92 +          val src_paths = Keyword.command_files cmd (Path.explode name);
   10.93 +        in map (Command.read_file master_dir pos) src_paths end
   10.94 +    | files => map Exn.release files));
   10.95 +
   10.96 +fun provide (src_path, id) =
   10.97 +  map_files (fn (master_dir, imports, provided) =>
   10.98 +    if AList.defined (op =) provided src_path then
   10.99 +      error ("Duplicate use of source file: " ^ Path.print src_path)
  10.100 +    else (master_dir, imports, (src_path, id) :: provided));
  10.101 +
  10.102 +fun provide_parse_files cmd =
  10.103 +  parse_files cmd >> (fn files => fn thy =>
  10.104 +    let
  10.105 +      val fs = files thy;
  10.106 +      val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
  10.107 +    in (fs, thy') end);
  10.108 +
  10.109 +fun load_file thy src_path =
  10.110 +  let
  10.111 +    val full_path = check_file (master_directory thy) src_path;
  10.112 +    val text = File.read full_path;
  10.113 +    val id = SHA1.digest text;
  10.114 +  in ((full_path, id), text) end;
  10.115 +
  10.116 +fun loaded_files_current thy =
  10.117 +  #provided (Files.get thy) |>
  10.118 +    forall (fn (src_path, id) =>
  10.119 +      (case try (load_file thy) src_path of
  10.120 +        NONE => false
  10.121 +      | SOME ((_, id'), _) => id = id'));
  10.122 +
  10.123 +(*Proof General legacy*)
  10.124 +fun loaded_files thy =
  10.125 +  let val {master_dir, provided, ...} = Files.get thy
  10.126 +  in map (File.full_path master_dir o #1) provided end;
  10.127 +
  10.128 +
  10.129 +(* load theory *)
  10.130 +
  10.131 +fun begin_theory master_dir {name, imports, keywords} parents =
  10.132 +  Theory.begin_theory name parents
  10.133 +  |> put_deps master_dir imports
  10.134 +  |> fold Thy_Header.declare_keyword keywords;
  10.135 +
  10.136 +fun excursion master_dir last_timing init elements =
  10.137 +  let
  10.138 +    fun prepare_span span =
  10.139 +      Thy_Syntax.span_content span
  10.140 +      |> Command.read init master_dir []
  10.141 +      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
  10.142 +
  10.143 +    fun element_result span_elem (st, _) =
  10.144 +      let
  10.145 +        val elem = Thy_Syntax.map_element prepare_span span_elem;
  10.146 +        val (results, st') = Toplevel.element_result elem st;
  10.147 +        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
  10.148 +      in (results, (st', pos')) end;
  10.149 +
  10.150 +    val (results, (end_state, end_pos)) =
  10.151 +      fold_map element_result elements (Toplevel.toplevel, Position.none);
  10.152 +
  10.153 +    val thy = Toplevel.end_theory end_pos end_state;
  10.154 +  in (results, thy) end;
  10.155 +
  10.156 +fun load_thy document last_timing update_time master_dir header text_pos text parents =
  10.157 +  let
  10.158 +    val time = ! Toplevel.timing;
  10.159 +
  10.160 +    val {name = (name, _), ...} = header;
  10.161 +    val _ = Thy_Header.define_keywords header;
  10.162 +
  10.163 +    val lexs = Keyword.get_lexicons ();
  10.164 +    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
  10.165 +    val spans = Thy_Syntax.parse_spans toks;
  10.166 +    val elements = Thy_Syntax.parse_elements spans;
  10.167 +
  10.168 +    fun init () =
  10.169 +      begin_theory master_dir header parents
  10.170 +      |> Present.begin_theory update_time
  10.171 +          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
  10.172 +
  10.173 +    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
  10.174 +    val (results, thy) =
  10.175 +      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
  10.176 +    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
  10.177 +
  10.178 +    fun present () =
  10.179 +      let
  10.180 +        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
  10.181 +        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
  10.182 +      in
  10.183 +        if exists (Toplevel.is_skipped_proof o #2) res then
  10.184 +          warning ("Cannot present theory with skipped proofs: " ^ quote name)
  10.185 +        else
  10.186 +          let val tex_source =
  10.187 +            Thy_Output.present_thy minor Keyword.command_tags
  10.188 +              (Outer_Syntax.is_markup outer_syntax) res toks
  10.189 +            |> Buffer.content;
  10.190 +          in if document then Present.theory_output name tex_source else () end
  10.191 +      end;
  10.192 +
  10.193 +  in (thy, present, size text) end;
  10.194 +
  10.195 +
  10.196 +(* antiquotations *)
  10.197 +
  10.198 +local
  10.199 +
  10.200 +fun check_path strict ctxt dir (name, pos) =
  10.201 +  let
  10.202 +    val _ = Context_Position.report ctxt pos Markup.language_path;
  10.203 +
  10.204 +    val path = Path.append dir (Path.explode name)
  10.205 +      handle ERROR msg => error (msg ^ Position.here pos);
  10.206 +
  10.207 +    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
  10.208 +    val _ =
  10.209 +      if can Path.expand path andalso File.exists path then ()
  10.210 +      else
  10.211 +        let
  10.212 +          val path' = perhaps (try Path.expand) path;
  10.213 +          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
  10.214 +        in
  10.215 +          if strict then error msg
  10.216 +          else
  10.217 +            Context_Position.if_visible ctxt Output.report
  10.218 +              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
  10.219 +        end;
  10.220 +  in path end;
  10.221 +
  10.222 +fun file_antiq strict ctxt (name, pos) =
  10.223 +  let
  10.224 +    val dir = master_directory (Proof_Context.theory_of ctxt);
  10.225 +    val _ = check_path strict ctxt dir (name, pos);
  10.226 +  in
  10.227 +    space_explode "/" name
  10.228 +    |> map Thy_Output.verb_text
  10.229 +    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
  10.230 +  end;
  10.231 +
  10.232 +in
  10.233 +
  10.234 +val _ = Theory.setup
  10.235 + (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
  10.236 +    (file_antiq true o #context) #>
  10.237 +  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
  10.238 +    (file_antiq false o #context) #>
  10.239 +  ML_Antiquotation.value @{binding path}
  10.240 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
  10.241 +      let val path = check_path true ctxt Path.current arg
  10.242 +      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
  10.243 +
  10.244 +end;
  10.245 +
  10.246 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/PIDE/resources.scala	Tue Mar 18 17:39:03 2014 +0100
    11.3 @@ -0,0 +1,111 @@
    11.4 +/*  Title:      Pure/PIDE/resources.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Resources for theories and auxiliary files.
    11.8 +*/
    11.9 +
   11.10 +package isabelle
   11.11 +
   11.12 +
   11.13 +import scala.annotation.tailrec
   11.14 +
   11.15 +import java.io.{File => JFile}
   11.16 +
   11.17 +
   11.18 +object Resources
   11.19 +{
   11.20 +  /* paths */
   11.21 +
   11.22 +  def thy_path(path: Path): Path = path.ext("thy")
   11.23 +
   11.24 +  def is_wellformed_thy_path(str: String): Boolean =
   11.25 +    try { thy_path(Path.explode(str)); true }
   11.26 +    catch { case ERROR(_) => false }
   11.27 +}
   11.28 +
   11.29 +
   11.30 +class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
   11.31 +{
   11.32 +  /* document node names */
   11.33 +
   11.34 +  def node_name(raw_path: Path): Document.Node.Name =
   11.35 +  {
   11.36 +    val path = raw_path.expand
   11.37 +    val node = path.implode
   11.38 +    val theory = Thy_Header.thy_name(node).getOrElse("")
   11.39 +    val master_dir = if (theory == "") "" else path.dir.implode
   11.40 +    Document.Node.Name(node, master_dir, theory)
   11.41 +  }
   11.42 +
   11.43 +
   11.44 +  /* file-system operations */
   11.45 +
   11.46 +  def append(dir: String, source_path: Path): String =
   11.47 +    (Path.explode(dir) + source_path).expand.implode
   11.48 +
   11.49 +  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   11.50 +  {
   11.51 +    val path = Path.explode(name.node)
   11.52 +    if (!path.is_file) error("No such file: " + path.toString)
   11.53 +
   11.54 +    val text = File.read(path)
   11.55 +    Symbol.decode_strict(text)
   11.56 +    f(text)
   11.57 +  }
   11.58 +
   11.59 +
   11.60 +  /* theory files */
   11.61 +
   11.62 +  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
   11.63 +    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   11.64 +
   11.65 +  def body_files(syntax: Outer_Syntax, text: String): List[String] =
   11.66 +  {
   11.67 +    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
   11.68 +    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
   11.69 +  }
   11.70 +
   11.71 +  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   11.72 +  {
   11.73 +    val theory = Thy_Header.base_name(s)
   11.74 +    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
   11.75 +    else {
   11.76 +      val path = Path.explode(s)
   11.77 +      val node = append(master.master_dir, Resources.thy_path(path))
   11.78 +      val master_dir = append(master.master_dir, path.dir)
   11.79 +      Document.Node.Name(node, master_dir, theory)
   11.80 +    }
   11.81 +  }
   11.82 +
   11.83 +  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   11.84 +  {
   11.85 +    try {
   11.86 +      val header = Thy_Header.read(text)
   11.87 +
   11.88 +      val name1 = header.name
   11.89 +      if (name.theory != name1)
   11.90 +        error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
   11.91 +          " for theory " + quote(name1))
   11.92 +
   11.93 +      val imports = header.imports.map(import_name(name, _))
   11.94 +      Document.Node.Header(imports, header.keywords, Nil)
   11.95 +    }
   11.96 +    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   11.97 +  }
   11.98 +
   11.99 +  def check_thy(name: Document.Node.Name): Document.Node.Header =
  11.100 +    with_thy_text(name, check_thy_text(name, _))
  11.101 +
  11.102 +
  11.103 +  /* theory text edits */
  11.104 +
  11.105 +  def text_edits(
  11.106 +    reparse_limit: Int,
  11.107 +    previous: Document.Version,
  11.108 +    doc_blobs: Document.Blobs,
  11.109 +    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
  11.110 +    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
  11.111 +
  11.112 +  def syntax_changed() { }
  11.113 +}
  11.114 +
    12.1 --- a/src/Pure/ROOT	Tue Mar 18 16:45:14 2014 +0100
    12.2 +++ b/src/Pure/ROOT	Tue Mar 18 17:39:03 2014 +0100
    12.3 @@ -161,6 +161,7 @@
    12.4      "PIDE/markup.ML"
    12.5      "PIDE/protocol.ML"
    12.6      "PIDE/query_operation.ML"
    12.7 +    "PIDE/resources.ML"
    12.8      "PIDE/xml.ML"
    12.9      "PIDE/yxml.ML"
   12.10      "Proof/extraction.ML"
   12.11 @@ -198,7 +199,6 @@
   12.12      "Thy/thm_deps.ML"
   12.13      "Thy/thy_header.ML"
   12.14      "Thy/thy_info.ML"
   12.15 -    "Thy/thy_load.ML"
   12.16      "Thy/thy_output.ML"
   12.17      "Thy/thy_syntax.ML"
   12.18      "Tools/build.ML"
    13.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 16:45:14 2014 +0100
    13.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 17:39:03 2014 +0100
    13.3 @@ -281,7 +281,7 @@
    13.4  use "Thy/present.ML";
    13.5  use "PIDE/command.ML";
    13.6  use "PIDE/query_operation.ML";
    13.7 -use "Thy/thy_load.ML";
    13.8 +use "PIDE/resources.ML";
    13.9  use "Thy/thy_info.ML";
   13.10  use "PIDE/document.ML";
   13.11  
    14.1 --- a/src/Pure/System/session.scala	Tue Mar 18 16:45:14 2014 +0100
    14.2 +++ b/src/Pure/System/session.scala	Tue Mar 18 17:39:03 2014 +0100
    14.3 @@ -109,7 +109,7 @@
    14.4  }
    14.5  
    14.6  
    14.7 -class Session(val thy_load: Thy_Load)
    14.8 +class Session(val resources: Resources)
    14.9  {
   14.10    /* global flags */
   14.11  
   14.12 @@ -180,8 +180,8 @@
   14.13          case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
   14.14            val prev = previous.get_finished
   14.15            val (syntax_changed, doc_edits, version) =
   14.16 -            Timing.timeit("Thy_Load.text_edits", timing) {
   14.17 -              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
   14.18 +            Timing.timeit("text_edits", timing) {
   14.19 +              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
   14.20              }
   14.21            version_result.fulfill(version)
   14.22            sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
   14.23 @@ -216,7 +216,7 @@
   14.24    def recent_syntax(): Outer_Syntax =
   14.25    {
   14.26      val version = current_state().recent_finished.version.get_finished
   14.27 -    if (version.is_init) thy_load.base_syntax
   14.28 +    if (version.is_init) resources.base_syntax
   14.29      else version.syntax
   14.30    }
   14.31  
   14.32 @@ -238,7 +238,7 @@
   14.33    def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   14.34    {
   14.35      val header1 =
   14.36 -      if (thy_load.loaded_theories(name.theory))
   14.37 +      if (resources.loaded_theories(name.theory))
   14.38          header.error("Cannot update finished theory " + quote(name.theory))
   14.39        else header
   14.40      (name, Document.Node.Deps(header1))
   14.41 @@ -401,7 +401,7 @@
   14.42        global_state >> (_.define_version(version, assignment))
   14.43        prover.get.update(previous.id, version.id, doc_edits)
   14.44  
   14.45 -      if (syntax_changed) thy_load.syntax_changed()
   14.46 +      if (syntax_changed) resources.syntax_changed()
   14.47      }
   14.48      //}}}
   14.49  
    15.1 --- a/src/Pure/Thy/thy_info.ML	Tue Mar 18 16:45:14 2014 +0100
    15.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Mar 18 17:39:03 2014 +0100
    15.3 @@ -123,13 +123,13 @@
    15.4      SOME theory => theory
    15.5    | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
    15.6  
    15.7 -val get_imports = Thy_Load.imports_of o get_theory;
    15.8 +val get_imports = Resources.imports_of o get_theory;
    15.9  
   15.10  (*Proof General legacy*)
   15.11  fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   15.12    (case get_deps name of
   15.13      NONE => []
   15.14 -  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
   15.15 +  | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
   15.16  
   15.17  
   15.18  
   15.19 @@ -284,7 +284,7 @@
   15.20  
   15.21      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
   15.22      val (theory, present, weight) =
   15.23 -      Thy_Load.load_thy document last_timing update_time dir header text_pos text
   15.24 +      Resources.load_thy document last_timing update_time dir header text_pos text
   15.25          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   15.26      fun commit () = update_thy deps theory;
   15.27    in
   15.28 @@ -295,18 +295,18 @@
   15.29    (case lookup_deps name of
   15.30      SOME NONE => (true, NONE, Position.none, get_imports name, [])
   15.31    | NONE =>
   15.32 -      let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name
   15.33 +      let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
   15.34        in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   15.35    | SOME (SOME {master, ...}) =>
   15.36        let
   15.37          val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   15.38 -          keywords = keywords'} = Thy_Load.check_thy dir name;
   15.39 +          keywords = keywords'} = Resources.check_thy dir name;
   15.40          val deps' = SOME (make_deps master' imports', text');
   15.41          val current =
   15.42            #2 master = #2 master' andalso
   15.43              (case lookup_theory name of
   15.44                NONE => false
   15.45 -            | SOME theory => Thy_Load.loaded_files_current theory);
   15.46 +            | SOME theory => Resources.loaded_files_current theory);
   15.47        in (current, deps', theory_pos', imports', keywords') end);
   15.48  
   15.49  in
   15.50 @@ -317,7 +317,7 @@
   15.51    let
   15.52      val path = Path.expand (Path.explode str);
   15.53      val name = Path.implode (Path.base path);
   15.54 -    val node_name = File.full_path dir (Thy_Load.thy_path path);
   15.55 +    val node_name = File.full_path dir (Resources.thy_path path);
   15.56      fun check_entry (Task (node_name', _, _)) =
   15.57            if node_name = node_name' then ()
   15.58            else
   15.59 @@ -384,7 +384,7 @@
   15.60      val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
   15.61      val _ = Thy_Header.define_keywords header;
   15.62      val parents = map (get_theory o base_name o fst) imports;
   15.63 -  in Thy_Load.begin_theory master_dir header parents end;
   15.64 +  in Resources.begin_theory master_dir header parents end;
   15.65  
   15.66  
   15.67  (* register theory *)
   15.68 @@ -392,8 +392,8 @@
   15.69  fun register_thy theory =
   15.70    let
   15.71      val name = Context.theory_name theory;
   15.72 -    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
   15.73 -    val imports = Thy_Load.imports_of theory;
   15.74 +    val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
   15.75 +    val imports = Resources.imports_of theory;
   15.76    in
   15.77      NAMED_CRITICAL "Thy_Info" (fn () =>
   15.78       (kill_thy name;
    16.1 --- a/src/Pure/Thy/thy_info.scala	Tue Mar 18 16:45:14 2014 +0100
    16.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Mar 18 17:39:03 2014 +0100
    16.3 @@ -10,7 +10,7 @@
    16.4  import java.util.concurrent.{Future => JFuture}
    16.5  
    16.6  
    16.7 -class Thy_Info(thy_load: Thy_Load)
    16.8 +class Thy_Info(resources: Resources)
    16.9  {
   16.10    /* messages */
   16.11  
   16.12 @@ -33,9 +33,9 @@
   16.13    {
   16.14      def load_files(syntax: Outer_Syntax): List[String] =
   16.15      {
   16.16 -      val string = thy_load.with_thy_text(name, _.toString)
   16.17 -      if (thy_load.body_files_test(syntax, string))
   16.18 -        thy_load.body_files(syntax, string)
   16.19 +      val string = resources.with_thy_text(name, _.toString)
   16.20 +      if (resources.body_files_test(syntax, string))
   16.21 +        resources.body_files(syntax, string)
   16.22        else Nil
   16.23      }
   16.24    }
   16.25 @@ -71,7 +71,7 @@
   16.26        val import_errors =
   16.27          (for {
   16.28            (theory, names) <- seen_names.iterator_list
   16.29 -          if !thy_load.loaded_theories(theory)
   16.30 +          if !resources.loaded_theories(theory)
   16.31            if names.length > 1
   16.32          } yield
   16.33            "Incoherent imports for theory " + quote(theory) + ":\n" +
   16.34 @@ -82,10 +82,10 @@
   16.35        header_errors ::: import_errors
   16.36      }
   16.37  
   16.38 -    lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   16.39 +    lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords)
   16.40  
   16.41      def loaded_theories: Set[String] =
   16.42 -      (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
   16.43 +      (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
   16.44  
   16.45      def load_files: List[Path] =
   16.46      {
   16.47 @@ -115,13 +115,13 @@
   16.48          required_by(initiators) + Position.here(require_pos)
   16.49  
   16.50      val required1 = required + thy
   16.51 -    if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory))
   16.52 +    if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
   16.53        required1
   16.54      else {
   16.55        try {
   16.56          if (initiators.contains(name)) error(cycle_msg(initiators))
   16.57          val header =
   16.58 -          try { thy_load.check_thy(name).cat_errors(message) }
   16.59 +          try { resources.check_thy(name).cat_errors(message) }
   16.60            catch { case ERROR(msg) => cat_error(msg, message) }
   16.61          val imports = header.imports.map((_, Position.File(name.node)))
   16.62          Dep(name, header) :: require_thys(name :: initiators, required1, imports)
    17.1 --- a/src/Pure/Thy/thy_load.ML	Tue Mar 18 16:45:14 2014 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,243 +0,0 @@
    17.4 -(*  Title:      Pure/Thy/thy_load.ML
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Management of theory sources and auxiliary files.
    17.8 -*)
    17.9 -
   17.10 -signature THY_LOAD =
   17.11 -sig
   17.12 -  val master_directory: theory -> Path.T
   17.13 -  val imports_of: theory -> (string * Position.T) list
   17.14 -  val thy_path: Path.T -> Path.T
   17.15 -  val check_thy: Path.T -> string ->
   17.16 -   {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
   17.17 -    imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   17.18 -  val parse_files: string -> (theory -> Token.file list) parser
   17.19 -  val provide: Path.T * SHA1.digest -> theory -> theory
   17.20 -  val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   17.21 -  val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   17.22 -  val loaded_files: theory -> Path.T list
   17.23 -  val loaded_files_current: theory -> bool
   17.24 -  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   17.25 -  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
   17.26 -    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
   17.27 -end;
   17.28 -
   17.29 -structure Thy_Load: THY_LOAD =
   17.30 -struct
   17.31 -
   17.32 -(* manage source files *)
   17.33 -
   17.34 -type files =
   17.35 - {master_dir: Path.T,  (*master directory of theory source*)
   17.36 -  imports: (string * Position.T) list,  (*source specification of imports*)
   17.37 -  provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
   17.38 -
   17.39 -fun make_files (master_dir, imports, provided): files =
   17.40 - {master_dir = master_dir, imports = imports, provided = provided};
   17.41 -
   17.42 -structure Files = Theory_Data
   17.43 -(
   17.44 -  type T = files;
   17.45 -  val empty = make_files (Path.current, [], []);
   17.46 -  fun extend _ = empty;
   17.47 -  fun merge _ = empty;
   17.48 -);
   17.49 -
   17.50 -fun map_files f =
   17.51 -  Files.map (fn {master_dir, imports, provided} =>
   17.52 -    make_files (f (master_dir, imports, provided)));
   17.53 -
   17.54 -
   17.55 -val master_directory = #master_dir o Files.get;
   17.56 -val imports_of = #imports o Files.get;
   17.57 -
   17.58 -fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
   17.59 -
   17.60 -
   17.61 -(* theory files *)
   17.62 -
   17.63 -val thy_path = Path.ext "thy";
   17.64 -
   17.65 -fun check_file dir file = File.check_file (File.full_path dir file);
   17.66 -
   17.67 -fun check_thy dir thy_name =
   17.68 -  let
   17.69 -    val path = thy_path (Path.basic thy_name);
   17.70 -    val master_file = check_file dir path;
   17.71 -    val text = File.read master_file;
   17.72 -
   17.73 -    val {name = (name, pos), imports, keywords} =
   17.74 -      Thy_Header.read (Path.position master_file) text;
   17.75 -    val _ = thy_name <> name andalso
   17.76 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
   17.77 -  in
   17.78 -   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
   17.79 -    imports = imports, keywords = keywords}
   17.80 -  end;
   17.81 -
   17.82 -
   17.83 -(* load files *)
   17.84 -
   17.85 -fun parse_files cmd =
   17.86 -  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
   17.87 -    (case Token.get_files tok of
   17.88 -      [] =>
   17.89 -        let
   17.90 -          val master_dir = master_directory thy;
   17.91 -          val pos = Token.pos_of tok;
   17.92 -          val src_paths = Keyword.command_files cmd (Path.explode name);
   17.93 -        in map (Command.read_file master_dir pos) src_paths end
   17.94 -    | files => map Exn.release files));
   17.95 -
   17.96 -fun provide (src_path, id) =
   17.97 -  map_files (fn (master_dir, imports, provided) =>
   17.98 -    if AList.defined (op =) provided src_path then
   17.99 -      error ("Duplicate use of source file: " ^ Path.print src_path)
  17.100 -    else (master_dir, imports, (src_path, id) :: provided));
  17.101 -
  17.102 -fun provide_parse_files cmd =
  17.103 -  parse_files cmd >> (fn files => fn thy =>
  17.104 -    let
  17.105 -      val fs = files thy;
  17.106 -      val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
  17.107 -    in (fs, thy') end);
  17.108 -
  17.109 -fun load_file thy src_path =
  17.110 -  let
  17.111 -    val full_path = check_file (master_directory thy) src_path;
  17.112 -    val text = File.read full_path;
  17.113 -    val id = SHA1.digest text;
  17.114 -  in ((full_path, id), text) end;
  17.115 -
  17.116 -fun loaded_files_current thy =
  17.117 -  #provided (Files.get thy) |>
  17.118 -    forall (fn (src_path, id) =>
  17.119 -      (case try (load_file thy) src_path of
  17.120 -        NONE => false
  17.121 -      | SOME ((_, id'), _) => id = id'));
  17.122 -
  17.123 -(*Proof General legacy*)
  17.124 -fun loaded_files thy =
  17.125 -  let val {master_dir, provided, ...} = Files.get thy
  17.126 -  in map (File.full_path master_dir o #1) provided end;
  17.127 -
  17.128 -
  17.129 -(* load theory *)
  17.130 -
  17.131 -fun begin_theory master_dir {name, imports, keywords} parents =
  17.132 -  Theory.begin_theory name parents
  17.133 -  |> put_deps master_dir imports
  17.134 -  |> fold Thy_Header.declare_keyword keywords;
  17.135 -
  17.136 -fun excursion master_dir last_timing init elements =
  17.137 -  let
  17.138 -    fun prepare_span span =
  17.139 -      Thy_Syntax.span_content span
  17.140 -      |> Command.read init master_dir []
  17.141 -      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
  17.142 -
  17.143 -    fun element_result span_elem (st, _) =
  17.144 -      let
  17.145 -        val elem = Thy_Syntax.map_element prepare_span span_elem;
  17.146 -        val (results, st') = Toplevel.element_result elem st;
  17.147 -        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
  17.148 -      in (results, (st', pos')) end;
  17.149 -
  17.150 -    val (results, (end_state, end_pos)) =
  17.151 -      fold_map element_result elements (Toplevel.toplevel, Position.none);
  17.152 -
  17.153 -    val thy = Toplevel.end_theory end_pos end_state;
  17.154 -  in (results, thy) end;
  17.155 -
  17.156 -fun load_thy document last_timing update_time master_dir header text_pos text parents =
  17.157 -  let
  17.158 -    val time = ! Toplevel.timing;
  17.159 -
  17.160 -    val {name = (name, _), ...} = header;
  17.161 -    val _ = Thy_Header.define_keywords header;
  17.162 -
  17.163 -    val lexs = Keyword.get_lexicons ();
  17.164 -    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
  17.165 -    val spans = Thy_Syntax.parse_spans toks;
  17.166 -    val elements = Thy_Syntax.parse_elements spans;
  17.167 -
  17.168 -    fun init () =
  17.169 -      begin_theory master_dir header parents
  17.170 -      |> Present.begin_theory update_time
  17.171 -          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
  17.172 -
  17.173 -    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
  17.174 -    val (results, thy) =
  17.175 -      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
  17.176 -    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
  17.177 -
  17.178 -    fun present () =
  17.179 -      let
  17.180 -        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
  17.181 -        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
  17.182 -      in
  17.183 -        if exists (Toplevel.is_skipped_proof o #2) res then
  17.184 -          warning ("Cannot present theory with skipped proofs: " ^ quote name)
  17.185 -        else
  17.186 -          let val tex_source =
  17.187 -            Thy_Output.present_thy minor Keyword.command_tags
  17.188 -              (Outer_Syntax.is_markup outer_syntax) res toks
  17.189 -            |> Buffer.content;
  17.190 -          in if document then Present.theory_output name tex_source else () end
  17.191 -      end;
  17.192 -
  17.193 -  in (thy, present, size text) end;
  17.194 -
  17.195 -
  17.196 -(* antiquotations *)
  17.197 -
  17.198 -local
  17.199 -
  17.200 -fun check_path strict ctxt dir (name, pos) =
  17.201 -  let
  17.202 -    val _ = Context_Position.report ctxt pos Markup.language_path;
  17.203 -
  17.204 -    val path = Path.append dir (Path.explode name)
  17.205 -      handle ERROR msg => error (msg ^ Position.here pos);
  17.206 -
  17.207 -    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
  17.208 -    val _ =
  17.209 -      if can Path.expand path andalso File.exists path then ()
  17.210 -      else
  17.211 -        let
  17.212 -          val path' = perhaps (try Path.expand) path;
  17.213 -          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
  17.214 -        in
  17.215 -          if strict then error msg
  17.216 -          else
  17.217 -            Context_Position.if_visible ctxt Output.report
  17.218 -              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
  17.219 -        end;
  17.220 -  in path end;
  17.221 -
  17.222 -fun file_antiq strict ctxt (name, pos) =
  17.223 -  let
  17.224 -    val dir = master_directory (Proof_Context.theory_of ctxt);
  17.225 -    val _ = check_path strict ctxt dir (name, pos);
  17.226 -  in
  17.227 -    space_explode "/" name
  17.228 -    |> map Thy_Output.verb_text
  17.229 -    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
  17.230 -  end;
  17.231 -
  17.232 -in
  17.233 -
  17.234 -val _ = Theory.setup
  17.235 - (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
  17.236 -    (file_antiq true o #context) #>
  17.237 -  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
  17.238 -    (file_antiq false o #context) #>
  17.239 -  ML_Antiquotation.value @{binding path}
  17.240 -    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
  17.241 -      let val path = check_path true ctxt Path.current arg
  17.242 -      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
  17.243 -
  17.244 -end;
  17.245 -
  17.246 -end;
    18.1 --- a/src/Pure/Thy/thy_load.scala	Tue Mar 18 16:45:14 2014 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,111 +0,0 @@
    18.4 -/*  Title:      Pure/Thy/thy_load.scala
    18.5 -    Author:     Makarius
    18.6 -
    18.7 -Primitives for loading theory files.
    18.8 -*/
    18.9 -
   18.10 -package isabelle
   18.11 -
   18.12 -
   18.13 -import scala.annotation.tailrec
   18.14 -
   18.15 -import java.io.{File => JFile}
   18.16 -
   18.17 -
   18.18 -object Thy_Load
   18.19 -{
   18.20 -  /* paths */
   18.21 -
   18.22 -  def thy_path(path: Path): Path = path.ext("thy")
   18.23 -
   18.24 -  def is_wellformed(str: String): Boolean =
   18.25 -    try { thy_path(Path.explode(str)); true }
   18.26 -    catch { case ERROR(_) => false }
   18.27 -}
   18.28 -
   18.29 -
   18.30 -class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
   18.31 -{
   18.32 -  /* document node names */
   18.33 -
   18.34 -  def node_name(raw_path: Path): Document.Node.Name =
   18.35 -  {
   18.36 -    val path = raw_path.expand
   18.37 -    val node = path.implode
   18.38 -    val theory = Thy_Header.thy_name(node).getOrElse("")
   18.39 -    val master_dir = if (theory == "") "" else path.dir.implode
   18.40 -    Document.Node.Name(node, master_dir, theory)
   18.41 -  }
   18.42 -
   18.43 -
   18.44 -  /* file-system operations */
   18.45 -
   18.46 -  def append(dir: String, source_path: Path): String =
   18.47 -    (Path.explode(dir) + source_path).expand.implode
   18.48 -
   18.49 -  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   18.50 -  {
   18.51 -    val path = Path.explode(name.node)
   18.52 -    if (!path.is_file) error("No such file: " + path.toString)
   18.53 -
   18.54 -    val text = File.read(path)
   18.55 -    Symbol.decode_strict(text)
   18.56 -    f(text)
   18.57 -  }
   18.58 -
   18.59 -
   18.60 -  /* theory files */
   18.61 -
   18.62 -  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
   18.63 -    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   18.64 -
   18.65 -  def body_files(syntax: Outer_Syntax, text: String): List[String] =
   18.66 -  {
   18.67 -    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
   18.68 -    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
   18.69 -  }
   18.70 -
   18.71 -  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   18.72 -  {
   18.73 -    val theory = Thy_Header.base_name(s)
   18.74 -    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
   18.75 -    else {
   18.76 -      val path = Path.explode(s)
   18.77 -      val node = append(master.master_dir, Thy_Load.thy_path(path))
   18.78 -      val master_dir = append(master.master_dir, path.dir)
   18.79 -      Document.Node.Name(node, master_dir, theory)
   18.80 -    }
   18.81 -  }
   18.82 -
   18.83 -  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   18.84 -  {
   18.85 -    try {
   18.86 -      val header = Thy_Header.read(text)
   18.87 -
   18.88 -      val name1 = header.name
   18.89 -      if (name.theory != name1)
   18.90 -        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
   18.91 -          " for theory " + quote(name1))
   18.92 -
   18.93 -      val imports = header.imports.map(import_name(name, _))
   18.94 -      Document.Node.Header(imports, header.keywords, Nil)
   18.95 -    }
   18.96 -    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   18.97 -  }
   18.98 -
   18.99 -  def check_thy(name: Document.Node.Name): Document.Node.Header =
  18.100 -    with_thy_text(name, check_thy_text(name, _))
  18.101 -
  18.102 -
  18.103 -  /* theory text edits */
  18.104 -
  18.105 -  def text_edits(
  18.106 -    reparse_limit: Int,
  18.107 -    previous: Document.Version,
  18.108 -    doc_blobs: Document.Blobs,
  18.109 -    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
  18.110 -    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
  18.111 -
  18.112 -  def syntax_changed() { }
  18.113 -}
  18.114 -
    19.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Mar 18 16:45:14 2014 +0100
    19.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Mar 18 17:39:03 2014 +0100
    19.3 @@ -257,7 +257,7 @@
    19.4      }
    19.5  
    19.6    def resolve_files(
    19.7 -      thy_load: Thy_Load,
    19.8 +      resources: Resources,
    19.9        syntax: Outer_Syntax,
   19.10        node_name: Document.Node.Name,
   19.11        span: List[Token],
   19.12 @@ -267,7 +267,7 @@
   19.13      span_files(syntax, span).map(file_name =>
   19.14        Exn.capture {
   19.15          val name =
   19.16 -          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
   19.17 +          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   19.18          val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
   19.19          (name, blob)
   19.20        })
   19.21 @@ -289,7 +289,7 @@
   19.22    }
   19.23  
   19.24    private def reparse_spans(
   19.25 -    thy_load: Thy_Load,
   19.26 +    resources: Resources,
   19.27      syntax: Outer_Syntax,
   19.28      doc_blobs: Document.Blobs,
   19.29      name: Document.Node.Name,
   19.30 @@ -299,7 +299,7 @@
   19.31      val cmds0 = commands.iterator(first, last).toList
   19.32      val blobs_spans0 =
   19.33        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
   19.34 -        map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
   19.35 +        map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span))
   19.36  
   19.37      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
   19.38  
   19.39 @@ -324,7 +324,7 @@
   19.40  
   19.41    // FIXME somewhat slow
   19.42    private def recover_spans(
   19.43 -    thy_load: Thy_Load,
   19.44 +    resources: Resources,
   19.45      syntax: Outer_Syntax,
   19.46      doc_blobs: Document.Blobs,
   19.47      name: Document.Node.Name,
   19.48 @@ -342,7 +342,7 @@
   19.49          case Some(first_unparsed) =>
   19.50            val first = next_invisible_command(cmds.reverse, first_unparsed)
   19.51            val last = next_invisible_command(cmds, first_unparsed)
   19.52 -          recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
   19.53 +          recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last))
   19.54          case None => cmds
   19.55        }
   19.56      recover(commands)
   19.57 @@ -352,7 +352,7 @@
   19.58    /* consolidate unfinished spans */
   19.59  
   19.60    private def consolidate_spans(
   19.61 -    thy_load: Thy_Load,
   19.62 +    resources: Resources,
   19.63      syntax: Outer_Syntax,
   19.64      doc_blobs: Document.Blobs,
   19.65      reparse_limit: Int,
   19.66 @@ -374,7 +374,7 @@
   19.67                  last = it.next
   19.68                  i += last.length
   19.69                }
   19.70 -              reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
   19.71 +              reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last)
   19.72              case None => commands
   19.73            }
   19.74          case None => commands
   19.75 @@ -396,7 +396,7 @@
   19.76    }
   19.77  
   19.78    private def text_edit(
   19.79 -    thy_load: Thy_Load,
   19.80 +    resources: Resources,
   19.81      syntax: Outer_Syntax,
   19.82      doc_blobs: Document.Blobs,
   19.83      reparse_limit: Int,
   19.84 @@ -413,7 +413,7 @@
   19.85            val commands0 = node.commands
   19.86            val commands1 = edit_text(text_edits, commands0)
   19.87            val commands2 =
   19.88 -            recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
   19.89 +            recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1)
   19.90            node.update_commands(commands2)
   19.91          }
   19.92  
   19.93 @@ -426,13 +426,13 @@
   19.94          if (node.same_perspective(perspective)) node
   19.95          else
   19.96            node.update_perspective(perspective).update_commands(
   19.97 -            consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
   19.98 +            consolidate_spans(resources, syntax, doc_blobs, reparse_limit,
   19.99                name, visible, node.commands))
  19.100      }
  19.101    }
  19.102  
  19.103    def text_edits(
  19.104 -      thy_load: Thy_Load,
  19.105 +      resources: Resources,
  19.106        reparse_limit: Int,
  19.107        previous: Document.Version,
  19.108        doc_blobs: Document.Blobs,
  19.109 @@ -440,7 +440,7 @@
  19.110      : (Boolean, List[Document.Edit_Command], Document.Version) =
  19.111    {
  19.112      val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
  19.113 -      header_edits(thy_load.base_syntax, previous, edits)
  19.114 +      header_edits(resources.base_syntax, previous, edits)
  19.115  
  19.116      if (edits.isEmpty)
  19.117        (false, Nil, Document.Version.make(syntax, previous.nodes))
  19.118 @@ -469,10 +469,10 @@
  19.119            val node1 =
  19.120              if (reparse_set(name) && !commands.isEmpty)
  19.121                node.update_commands(
  19.122 -                reparse_spans(thy_load, syntax, doc_blobs,
  19.123 +                reparse_spans(resources, syntax, doc_blobs,
  19.124                    name, commands, commands.head, commands.last))
  19.125              else node
  19.126 -          val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
  19.127 +          val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
  19.128  
  19.129            if (!(node.same_perspective(node2.perspective)))
  19.130              doc_edits += (name -> node2.perspective)
    20.1 --- a/src/Pure/Tools/build.scala	Tue Mar 18 16:45:14 2014 +0100
    20.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 18 17:39:03 2014 +0100
    20.3 @@ -419,8 +419,8 @@
    20.4                    val parent = deps(parent_name)
    20.5                    (parent.loaded_theories, parent.syntax)
    20.6                }
    20.7 -            val thy_load = new Thy_Load(preloaded, parent_syntax)
    20.8 -            val thy_info = new Thy_Info(thy_load)
    20.9 +            val resources = new Resources(preloaded, parent_syntax)
   20.10 +            val thy_info = new Thy_Info(resources)
   20.11  
   20.12              if (verbose || list_files) {
   20.13                val groups =
   20.14 @@ -432,7 +432,7 @@
   20.15              val thy_deps =
   20.16                thy_info.dependencies(
   20.17                  info.theories.map(_._2).flatten.
   20.18 -                  map(thy => (thy_load.node_name(info.dir + Thy_Load.thy_path(thy)), info.pos)))
   20.19 +                  map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos)))
   20.20  
   20.21              thy_deps.errors match {
   20.22                case Nil =>
    21.1 --- a/src/Pure/Tools/proof_general.ML	Tue Mar 18 16:45:14 2014 +0100
    21.2 +++ b/src/Pure/Tools/proof_general.ML	Tue Mar 18 17:39:03 2014 +0100
    21.3 @@ -337,7 +337,7 @@
    21.4        Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
    21.5          handle ERROR msg =>
    21.6            (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
    21.7 -            tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
    21.8 +            tell_file_retracted (Resources.thy_path (Path.basic name)))
    21.9      val _ = Isar.init ();
   21.10    in () end;
   21.11  
    22.1 --- a/src/Pure/build-jars	Tue Mar 18 16:45:14 2014 +0100
    22.2 +++ b/src/Pure/build-jars	Tue Mar 18 17:39:03 2014 +0100
    22.3 @@ -53,6 +53,7 @@
    22.4    PIDE/markup_tree.scala
    22.5    PIDE/protocol.scala
    22.6    PIDE/query_operation.scala
    22.7 +  PIDE/resources.scala
    22.8    PIDE/text.scala
    22.9    PIDE/xml.scala
   22.10    PIDE/yxml.scala
   22.11 @@ -73,7 +74,6 @@
   22.12    Thy/present.scala
   22.13    Thy/thy_header.scala
   22.14    Thy/thy_info.scala
   22.15 -  Thy/thy_load.scala
   22.16    Thy/thy_syntax.scala
   22.17    Tools/build.scala
   22.18    Tools/doc.scala
    23.1 --- a/src/Pure/pure_syn.ML	Tue Mar 18 16:45:14 2014 +0100
    23.2 +++ b/src/Pure/pure_syn.ML	Tue Mar 18 17:39:03 2014 +0100
    23.3 @@ -18,10 +18,10 @@
    23.4  val _ =
    23.5    Outer_Syntax.command
    23.6      (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
    23.7 -    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    23.8 +    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    23.9          let
   23.10            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
   23.11 -          val provide = Thy_Load.provide (src_path, digest);
   23.12 +          val provide = Resources.provide (src_path, digest);
   23.13            val source = {delimited = true, text = cat_lines lines, pos = pos};
   23.14          in
   23.15            gthy
    24.1 --- a/src/Tools/Code/code_runtime.ML	Tue Mar 18 16:45:14 2014 +0100
    24.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Mar 18 17:39:03 2014 +0100
    24.3 @@ -325,7 +325,7 @@
    24.4        let
    24.5          val preamble =
    24.6            "(* Generated from " ^
    24.7 -            Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
    24.8 +            Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
    24.9            "; DO NOT EDIT! *)";
   24.10          val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
   24.11        in
    25.1 --- a/src/Tools/Code/code_target.ML	Tue Mar 18 16:45:14 2014 +0100
    25.2 +++ b/src/Tools/Code/code_target.ML	Tue Mar 18 17:39:03 2014 +0100
    25.3 @@ -380,7 +380,8 @@
    25.4    | assert_module_name module_name = module_name;
    25.5  
    25.6  fun using_master_directory ctxt =
    25.7 -  Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory (Proof_Context.theory_of ctxt)));
    25.8 +  Option.map (Path.append (File.pwd ()) o
    25.9 +    Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
   25.10  
   25.11  in
   25.12  
    26.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 18 16:45:14 2014 +0100
    26.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 18 17:39:03 2014 +0100
    26.3 @@ -27,7 +27,7 @@
    26.4    "src/jedit_editor.scala"
    26.5    "src/jedit_lib.scala"
    26.6    "src/jedit_options.scala"
    26.7 -  "src/jedit_thy_load.scala"
    26.8 +  "src/jedit_resources.scala"
    26.9    "src/monitor_dockable.scala"
   26.10    "src/output_dockable.scala"
   26.11    "src/plugin.scala"
    27.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 18 16:45:14 2014 +0100
    27.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 18 17:39:03 2014 +0100
    27.3 @@ -70,7 +70,7 @@
    27.4      if (is_theory) {
    27.5        JEdit_Lib.buffer_lock(buffer) {
    27.6          Exn.capture {
    27.7 -          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    27.8 +          PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    27.9          } match {
   27.10            case Exn.Res(header) => header
   27.11            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
   27.12 @@ -150,7 +150,7 @@
   27.13            _blob match {
   27.14              case Some(x) => x
   27.15              case None =>
   27.16 -              val bytes = PIDE.thy_load.file_content(buffer)
   27.17 +              val bytes = PIDE.resources.file_content(buffer)
   27.18                val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
   27.19                _blob = Some((bytes, file))
   27.20                (bytes, file)
    28.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Tue Mar 18 16:45:14 2014 +0100
    28.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Tue Mar 18 17:39:03 2014 +0100
    28.3 @@ -131,7 +131,7 @@
    28.4  
    28.5    private val context_entries =
    28.6      new Context_Entry("", "current context") ::
    28.7 -      PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
    28.8 +      PIDE.resources.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
    28.9  
   28.10    private val context = new ComboBox[Context_Entry](context_entries) {
   28.11      tooltip = "Search in pre-loaded theory (default: context of current command)"
    29.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Mar 18 16:45:14 2014 +0100
    29.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Mar 18 17:39:03 2014 +0100
    29.3 @@ -133,7 +133,7 @@
    29.4  
    29.5  
    29.6  class Isabelle_Sidekick_Default extends
    29.7 -  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
    29.8 +  Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
    29.9  
   29.10  
   29.11  class Isabelle_Sidekick_Options extends
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 18 17:39:03 2014 +0100
    30.3 @@ -0,0 +1,123 @@
    30.4 +/*  Title:      Tools/jEdit/src/jedit_resources.scala
    30.5 +    Author:     Makarius
    30.6 +
    30.7 +Resources for theories and auxiliary files, based on jEdit buffer
    30.8 +content and virtual file-systems.
    30.9 +*/
   30.10 +
   30.11 +package isabelle.jedit
   30.12 +
   30.13 +
   30.14 +import isabelle._
   30.15 +
   30.16 +import java.io.{File => JFile, IOException, ByteArrayOutputStream}
   30.17 +import javax.swing.text.Segment
   30.18 +
   30.19 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
   30.20 +import org.gjt.sp.jedit.MiscUtilities
   30.21 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
   30.22 +import org.gjt.sp.jedit.bufferio.BufferIORequest
   30.23 +
   30.24 +
   30.25 +class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
   30.26 +  extends Resources(loaded_theories, base_syntax)
   30.27 +{
   30.28 +  /* document node names */
   30.29 +
   30.30 +  def node_name(buffer: Buffer): Document.Node.Name =
   30.31 +  {
   30.32 +    val node = JEdit_Lib.buffer_name(buffer)
   30.33 +    val theory = Thy_Header.thy_name(node).getOrElse("")
   30.34 +    val master_dir = if (theory == "") "" else buffer.getDirectory
   30.35 +    Document.Node.Name(node, master_dir, theory)
   30.36 +  }
   30.37 +
   30.38 +  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   30.39 +  {
   30.40 +    val name = node_name(buffer)
   30.41 +    if (name.is_theory) Some(name) else None
   30.42 +  }
   30.43 +
   30.44 +
   30.45 +  /* file-system operations */
   30.46 +
   30.47 +  override def append(dir: String, source_path: Path): String =
   30.48 +  {
   30.49 +    val path = source_path.expand
   30.50 +    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
   30.51 +    else {
   30.52 +      val vfs = VFSManager.getVFSForPath(dir)
   30.53 +      if (vfs.isInstanceOf[FileVFS])
   30.54 +        MiscUtilities.resolveSymlinks(
   30.55 +          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
   30.56 +      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
   30.57 +    }
   30.58 +  }
   30.59 +
   30.60 +  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   30.61 +  {
   30.62 +    Swing_Thread.now {
   30.63 +      JEdit_Lib.jedit_buffer(name.node) match {
   30.64 +        case Some(buffer) =>
   30.65 +          JEdit_Lib.buffer_lock(buffer) {
   30.66 +            Some(f(buffer.getSegment(0, buffer.getLength)))
   30.67 +          }
   30.68 +        case None => None
   30.69 +      }
   30.70 +    } getOrElse {
   30.71 +      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
   30.72 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   30.73 +      f(File.read(file))
   30.74 +    }
   30.75 +  }
   30.76 +
   30.77 +  def check_file(view: View, path: String): Boolean =
   30.78 +  {
   30.79 +    val vfs = VFSManager.getVFSForPath(path)
   30.80 +    val session = vfs.createVFSSession(path, view)
   30.81 +
   30.82 +    try {
   30.83 +      session != null && {
   30.84 +        try {
   30.85 +          val file = vfs._getFile(session, path, view)
   30.86 +          file != null && file.isReadable && file.getType == VFSFile.FILE
   30.87 +        }
   30.88 +        catch { case _: IOException => false }
   30.89 +      }
   30.90 +    }
   30.91 +    finally {
   30.92 +      try { vfs._endVFSSession(session, view) }
   30.93 +      catch { case _: IOException => }
   30.94 +    }
   30.95 +  }
   30.96 +
   30.97 +
   30.98 +  /* file content */
   30.99 +
  30.100 +  def file_content(buffer: Buffer): Bytes =
  30.101 +  {
  30.102 +    val path = buffer.getPath
  30.103 +    val vfs = VFSManager.getVFSForPath(path)
  30.104 +    val content =
  30.105 +      new BufferIORequest(null, buffer, null, vfs, path) {
  30.106 +        def _run() { }
  30.107 +        def apply(): Bytes =
  30.108 +        {
  30.109 +          val out =
  30.110 +            new ByteArrayOutputStream(buffer.getLength + 1) {
  30.111 +              def content(): Bytes = Bytes(this.buf, 0, this.count)
  30.112 +            }
  30.113 +          write(buffer, out)
  30.114 +          out.content()
  30.115 +        }
  30.116 +      }
  30.117 +    content()
  30.118 +  }
  30.119 +
  30.120 +
  30.121 +  /* theory text edits */
  30.122 +
  30.123 +  override def syntax_changed(): Unit =
  30.124 +    Swing_Thread.later { jEdit.propertiesChanged() }
  30.125 +}
  30.126 +
    31.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Mar 18 16:45:14 2014 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,121 +0,0 @@
    31.4 -/*  Title:      Tools/jEdit/src/jedit_thy_load.scala
    31.5 -    Author:     Makarius
    31.6 -
    31.7 -Primitives for loading theory files, based on jEdit buffer content.
    31.8 -*/
    31.9 -
   31.10 -package isabelle.jedit
   31.11 -
   31.12 -
   31.13 -import isabelle._
   31.14 -
   31.15 -import java.io.{File => JFile, IOException, ByteArrayOutputStream}
   31.16 -import javax.swing.text.Segment
   31.17 -
   31.18 -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
   31.19 -import org.gjt.sp.jedit.MiscUtilities
   31.20 -import org.gjt.sp.jedit.{jEdit, View, Buffer}
   31.21 -import org.gjt.sp.jedit.bufferio.BufferIORequest
   31.22 -
   31.23 -class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
   31.24 -  extends Thy_Load(loaded_theories, base_syntax)
   31.25 -{
   31.26 -  /* document node names */
   31.27 -
   31.28 -  def node_name(buffer: Buffer): Document.Node.Name =
   31.29 -  {
   31.30 -    val node = JEdit_Lib.buffer_name(buffer)
   31.31 -    val theory = Thy_Header.thy_name(node).getOrElse("")
   31.32 -    val master_dir = if (theory == "") "" else buffer.getDirectory
   31.33 -    Document.Node.Name(node, master_dir, theory)
   31.34 -  }
   31.35 -
   31.36 -  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   31.37 -  {
   31.38 -    val name = node_name(buffer)
   31.39 -    if (name.is_theory) Some(name) else None
   31.40 -  }
   31.41 -
   31.42 -
   31.43 -  /* file-system operations */
   31.44 -
   31.45 -  override def append(dir: String, source_path: Path): String =
   31.46 -  {
   31.47 -    val path = source_path.expand
   31.48 -    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
   31.49 -    else {
   31.50 -      val vfs = VFSManager.getVFSForPath(dir)
   31.51 -      if (vfs.isInstanceOf[FileVFS])
   31.52 -        MiscUtilities.resolveSymlinks(
   31.53 -          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
   31.54 -      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
   31.55 -    }
   31.56 -  }
   31.57 -
   31.58 -  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   31.59 -  {
   31.60 -    Swing_Thread.now {
   31.61 -      JEdit_Lib.jedit_buffer(name.node) match {
   31.62 -        case Some(buffer) =>
   31.63 -          JEdit_Lib.buffer_lock(buffer) {
   31.64 -            Some(f(buffer.getSegment(0, buffer.getLength)))
   31.65 -          }
   31.66 -        case None => None
   31.67 -      }
   31.68 -    } getOrElse {
   31.69 -      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
   31.70 -      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   31.71 -      f(File.read(file))
   31.72 -    }
   31.73 -  }
   31.74 -
   31.75 -  def check_file(view: View, path: String): Boolean =
   31.76 -  {
   31.77 -    val vfs = VFSManager.getVFSForPath(path)
   31.78 -    val session = vfs.createVFSSession(path, view)
   31.79 -
   31.80 -    try {
   31.81 -      session != null && {
   31.82 -        try {
   31.83 -          val file = vfs._getFile(session, path, view)
   31.84 -          file != null && file.isReadable && file.getType == VFSFile.FILE
   31.85 -        }
   31.86 -        catch { case _: IOException => false }
   31.87 -      }
   31.88 -    }
   31.89 -    finally {
   31.90 -      try { vfs._endVFSSession(session, view) }
   31.91 -      catch { case _: IOException => }
   31.92 -    }
   31.93 -  }
   31.94 -
   31.95 -
   31.96 -  /* file content */
   31.97 -
   31.98 -  def file_content(buffer: Buffer): Bytes =
   31.99 -  {
  31.100 -    val path = buffer.getPath
  31.101 -    val vfs = VFSManager.getVFSForPath(path)
  31.102 -    val content =
  31.103 -      new BufferIORequest(null, buffer, null, vfs, path) {
  31.104 -        def _run() { }
  31.105 -        def apply(): Bytes =
  31.106 -        {
  31.107 -          val out =
  31.108 -            new ByteArrayOutputStream(buffer.getLength + 1) {
  31.109 -              def content(): Bytes = Bytes(this.buf, 0, this.count)
  31.110 -            }
  31.111 -          write(buffer, out)
  31.112 -          out.content()
  31.113 -        }
  31.114 -      }
  31.115 -    content()
  31.116 -  }
  31.117 -
  31.118 -
  31.119 -  /* theory text edits */
  31.120 -
  31.121 -  override def syntax_changed(): Unit =
  31.122 -    Swing_Thread.later { jEdit.propertiesChanged() }
  31.123 -}
  31.124 -
    32.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 18 16:45:14 2014 +0100
    32.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 18 17:39:03 2014 +0100
    32.3 @@ -36,12 +36,12 @@
    32.4    @volatile var startup_notified = false
    32.5  
    32.6    @volatile var plugin: Plugin = null
    32.7 -  @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
    32.8 +  @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
    32.9  
   32.10    def options_changed() { plugin.options_changed() }
   32.11  
   32.12 -  def thy_load(): JEdit_Thy_Load =
   32.13 -    session.thy_load.asInstanceOf[JEdit_Thy_Load]
   32.14 +  def resources(): JEdit_Resources =
   32.15 +    session.resources.asInstanceOf[JEdit_Resources]
   32.16  
   32.17    lazy val editor = new JEdit_Editor
   32.18  
   32.19 @@ -109,7 +109,7 @@
   32.20          if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED)
   32.21        } {
   32.22          JEdit_Lib.buffer_lock(buffer) {
   32.23 -          val node_name = thy_load.node_name(buffer)
   32.24 +          val node_name = resources.node_name(buffer)
   32.25            val model =
   32.26              document_model(buffer) match {
   32.27                case Some(model) if model.node_name == node_name => model
   32.28 @@ -202,10 +202,10 @@
   32.29                if model.is_theory
   32.30              } yield (model.node_name, Position.none)
   32.31  
   32.32 -          val thy_info = new Thy_Info(PIDE.thy_load)
   32.33 +          val thy_info = new Thy_Info(PIDE.resources)
   32.34            // FIXME avoid I/O in Swing thread!?!
   32.35            val files = thy_info.dependencies(thys).deps.map(_.name.node).
   32.36 -            filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
   32.37 +            filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   32.38  
   32.39            if (!files.isEmpty) {
   32.40              if (PIDE.options.bool("jedit_auto_load")) {
   32.41 @@ -349,9 +349,9 @@
   32.42        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   32.43  
   32.44        val content = Isabelle_Logic.session_content(false)
   32.45 -      val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   32.46 +      val resources = new JEdit_Resources(content.loaded_theories, content.syntax)
   32.47  
   32.48 -      PIDE.session = new Session(thy_load) {
   32.49 +      PIDE.session = new Session(resources) {
   32.50          override def output_delay = PIDE.options.seconds("editor_output_delay")
   32.51          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   32.52        }
    33.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 16:45:14 2014 +0100
    33.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 17:39:03 2014 +0100
    33.3 @@ -336,7 +336,7 @@
    33.4          {
    33.5            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    33.6            if Path.is_valid(name) =>
    33.7 -            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    33.8 +            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    33.9              val link = PIDE.editor.hyperlink_file(jedit_file)
   33.10              Some(links :+ Text.Info(snapshot.convert(info_range), link))
   33.11  
   33.12 @@ -470,7 +470,7 @@
   33.13              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   33.14            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   33.15            if Path.is_valid(name) =>
   33.16 -            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
   33.17 +            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
   33.18              val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
   33.19              Some(add(prev, r, (true, XML.Text(text))))
   33.20            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    34.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 18 16:45:14 2014 +0100
    34.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Mar 18 17:39:03 2014 +0100
    34.3 @@ -192,7 +192,7 @@
    34.4        }).filter(_._1.is_theory)
    34.5      val nodes_status1 =
    34.6        (nodes_status /: iterator)({ case (status, (name, node)) =>
    34.7 -          if (PIDE.thy_load.loaded_theories(name.theory)) status
    34.8 +          if (PIDE.resources.loaded_theories(name.theory)) status
    34.9            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   34.10  
   34.11      if (nodes_status != nodes_status1) {
    35.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 18 16:45:14 2014 +0100
    35.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 18 17:39:03 2014 +0100
    35.3 @@ -186,7 +186,7 @@
    35.4        }
    35.5      val nodes_timing1 =
    35.6        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
    35.7 -          if (PIDE.thy_load.loaded_theories(name.theory)) timing1
    35.8 +          if (PIDE.resources.loaded_theories(name.theory)) timing1
    35.9            else {
   35.10              val node_timing =
   35.11                Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)