load files that are not provided by PIDE blobs;
authorwenzelm
Wed Nov 20 11:55:52 2013 +0100 (2013-11-20)
changeset 5452692961f196d9e
parent 54525 de7c13e25212
child 54527 bfeb0ea6c2c0
load files that are not provided by PIDE blobs;
uniform resolve_files via Command.read;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Nov 20 10:51:47 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Nov 20 11:55:52 2013 +0100
     1.3 @@ -6,14 +6,15 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type blob = (string * string) Exn.result
     1.8 -  val read: (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition
     1.9 +  type blob = (string * string option) Exn.result
    1.10 +  val read_file: Path.T -> Position.T -> Path.T -> Token.file
    1.11 +  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
    1.12    type eval
    1.13    val eval_eq: eval * eval -> bool
    1.14    val eval_running: eval -> bool
    1.15    val eval_finished: eval -> bool
    1.16    val eval_result_state: eval -> Toplevel.state
    1.17 -  val eval: (unit -> theory) -> blob list -> Token.T list -> eval -> eval
    1.18 +  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
    1.19    type print
    1.20    val print: bool -> (string * string list) list -> string ->
    1.21      eval -> print list -> print list option
    1.22 @@ -83,15 +84,23 @@
    1.23  
    1.24  (* read *)
    1.25  
    1.26 -type blob = (string * string) Exn.result;  (*file node name, digest or text*)
    1.27 +type blob = (string * string option) Exn.result;  (*file node name, digest or text*)
    1.28  
    1.29 -fun resolve_files blobs toks =
    1.30 +fun read_file master_dir pos src_path =
    1.31 +  let
    1.32 +    val full_path = File.check_file (File.full_path master_dir src_path);
    1.33 +    val _ = Position.report pos (Markup.path (Path.implode full_path));
    1.34 +  in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
    1.35 +
    1.36 +fun resolve_files master_dir blobs toks =
    1.37    (case Thy_Syntax.parse_spans toks of
    1.38      [span] => span
    1.39        |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    1.40          let
    1.41 -          fun make_file src_path (Exn.Res (file, text)) =
    1.42 -                let val _ = Position.report pos (Markup.path file);
    1.43 +          fun make_file src_path (Exn.Res (_, NONE)) =
    1.44 +                Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.45 +            | make_file src_path (Exn.Res (file, SOME text)) =
    1.46 +                let val _ = Position.report pos (Markup.path file)
    1.47                  in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
    1.48              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.49  
    1.50 @@ -105,7 +114,7 @@
    1.51        |> Thy_Syntax.span_content
    1.52    | _ => toks);
    1.53  
    1.54 -fun read init blobs span =
    1.55 +fun read init master_dir blobs span =
    1.56    let
    1.57      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    1.58      val command_reports = Outer_Syntax.command_reports outer_syntax;
    1.59 @@ -122,7 +131,7 @@
    1.60    in
    1.61      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.62      else
    1.63 -      (case Outer_Syntax.read_spans outer_syntax (resolve_files blobs span) of
    1.64 +      (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
    1.65          [tr] =>
    1.66            if Keyword.is_control (Toplevel.name_of tr) then
    1.67              Toplevel.malformed pos "Illegal control command"
    1.68 @@ -203,14 +212,14 @@
    1.69  
    1.70  in
    1.71  
    1.72 -fun eval init blobs span eval0 =
    1.73 +fun eval init master_dir blobs span eval0 =
    1.74    let
    1.75      val exec_id = Document_ID.make ();
    1.76      fun process () =
    1.77        let
    1.78          val tr =
    1.79            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    1.80 -            (fn () => read init blobs span |> Toplevel.exec_id exec_id) ();
    1.81 +            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
    1.82        in eval_state span tr (eval_result eval0) end;
    1.83    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    1.84  
     2.1 --- a/src/Pure/PIDE/document.ML	Wed Nov 20 10:51:47 2013 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed Nov 20 11:55:52 2013 +0100
     2.3 @@ -90,9 +90,14 @@
     2.4  
     2.5  fun read_header node span =
     2.6    let
     2.7 -    val (dir, {name = (name, _), imports, keywords}) = get_header node;
     2.8 +    val {name = (name, _), imports, keywords} = #2 (get_header node);
     2.9      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    2.10 -  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
    2.11 +  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    2.12 +
    2.13 +fun master_directory node =
    2.14 +  (case try Url.explode (#1 (get_header node)) of
    2.15 +    SOME (Url.File path) => path
    2.16 +  | _ => Path.current);
    2.17  
    2.18  fun get_perspective (Node {perspective, ...}) = perspective;
    2.19  fun set_perspective args =
    2.20 @@ -329,7 +334,7 @@
    2.21      val blobs' =
    2.22        (commands', Symtab.empty) |->
    2.23          Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    2.24 -          fold (fn Exn.Res (_, digest) => Symtab.update (digest, the_blob state digest) | _ => I));
    2.25 +          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    2.26  
    2.27    in (versions', blobs', commands', execution) end);
    2.28  
    2.29 @@ -421,12 +426,8 @@
    2.30  
    2.31  fun init_theory deps node span =
    2.32    let
    2.33 -    (* FIXME provide files via Isabelle/Scala, not master_dir *)
    2.34 -    val (dir, header) = read_header node span;
    2.35 -    val master_dir =
    2.36 -      (case try Url.explode dir of
    2.37 -        SOME (Url.File path) => path
    2.38 -      | _ => Path.current);
    2.39 +    val master_dir = master_directory node;
    2.40 +    val header = read_header node span;
    2.41      val imports = #imports header;
    2.42      val parents =
    2.43        imports |> map (fn (import, _) =>
    2.44 @@ -500,11 +501,12 @@
    2.45        val command_visible = visible_command node command_id';
    2.46        val command_overlays = overlays node command_id';
    2.47        val (command_name, blobs0, span0) = the_command state command_id';
    2.48 -      val blobs = map (Exn.map_result (apsnd (the_blob state))) blobs0;
    2.49 +      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
    2.50        val span = Lazy.force span0;
    2.51  
    2.52        val eval' =
    2.53 -        Command.eval (fn () => the_default illegal_init init span) blobs span eval;
    2.54 +        Command.eval (fn () => the_default illegal_init init span)
    2.55 +          (master_directory node) blobs span eval;
    2.56        val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
    2.57        val exec' = (eval', prints');
    2.58  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Wed Nov 20 10:51:47 2013 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Nov 20 11:55:52 2013 +0100
     3.3 @@ -34,8 +34,8 @@
     3.4            YXML.parse_body blobs_yxml |>
     3.5              let open XML.Decode in
     3.6                list (variant
     3.7 -               [fn ([a, b], []) => Exn.Res (a, b),
     3.8 -                fn ([a], []) => Exn.Exn (ERROR a)])
     3.9 +               [fn ([], a) => Exn.Res (pair string (option string) a),
    3.10 +                fn ([], a) => Exn.Exn (ERROR (string a))])
    3.11              end;
    3.12        in
    3.13          Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
     4.1 --- a/src/Pure/PIDE/protocol.scala	Wed Nov 20 10:51:47 2013 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Nov 20 11:55:52 2013 +0100
     4.3 @@ -322,9 +322,9 @@
     4.4      { import XML.Encode._
     4.5        val encode_blob: T[Command.Blob] =
     4.6          variant(List(
     4.7 -          { case Exn.Res((a, Some(b))) => (List(a.node, b.toString), Nil) },
     4.8 -          { case Exn.Res((a, None)) => (List("Missing file: " + quote(a.toString)), Nil)
     4.9 -            case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
    4.10 +          { case Exn.Res((a, b)) =>
    4.11 +              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
    4.12 +          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    4.13        YXML.string_of_body(list(encode_blob)(command.blobs))
    4.14      }
    4.15      protocol_command("Document.define_command",
     5.1 --- a/src/Pure/Thy/thy_load.ML	Wed Nov 20 10:51:47 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Nov 20 11:55:52 2013 +0100
     5.3 @@ -77,29 +77,19 @@
     5.4    end;
     5.5  
     5.6  
     5.7 -(* inlined files *)
     5.8 -
     5.9 -fun read_files dir cmd (path, pos) =
    5.10 -  let
    5.11 -    fun make_file src_path =
    5.12 -      let
    5.13 -        val full_path = check_file dir src_path;
    5.14 -        val _ = Position.report pos (Markup.path (Path.implode full_path));
    5.15 -      in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
    5.16 -  in map make_file (Keyword.command_files cmd path) end;
    5.17 +(* load files *)
    5.18  
    5.19  fun parse_files cmd =
    5.20    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
    5.21      (case Token.get_files tok of
    5.22 -      [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
    5.23 +      [] =>
    5.24 +        let
    5.25 +          val master_dir = master_directory thy;
    5.26 +          val pos = Token.position_of tok;
    5.27 +          val src_paths = Keyword.command_files cmd (Path.explode name);
    5.28 +        in map (Command.read_file master_dir pos) src_paths end
    5.29      | files => map Exn.release files));
    5.30  
    5.31 -fun resolve_files master_dir =
    5.32 -  Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir);
    5.33 -
    5.34 -
    5.35 -(* load files *)
    5.36 -
    5.37  fun provide (src_path, id) =
    5.38    map_files (fn (master_dir, imports, provided) =>
    5.39      if AList.defined (op =) provided src_path then
    5.40 @@ -140,11 +130,11 @@
    5.41    |> put_deps master_dir imports
    5.42    |> fold Thy_Header.declare_keyword keywords;
    5.43  
    5.44 -fun excursion last_timing init elements =
    5.45 +fun excursion master_dir last_timing init elements =
    5.46    let
    5.47      fun prepare_span span =
    5.48        Thy_Syntax.span_content span
    5.49 -      |> Command.read init []
    5.50 +      |> Command.read init master_dir []
    5.51        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    5.52  
    5.53      fun element_result span_elem (st, _) =
    5.54 @@ -169,7 +159,7 @@
    5.55  
    5.56      val lexs = Keyword.get_lexicons ();
    5.57      val toks = Thy_Syntax.parse_tokens lexs text_pos text;
    5.58 -    val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
    5.59 +    val spans = Thy_Syntax.parse_spans toks;
    5.60      val elements = Thy_Syntax.parse_elements spans;
    5.61  
    5.62      fun init () =
    5.63 @@ -178,7 +168,8 @@
    5.64            (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    5.65  
    5.66      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    5.67 -    val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
    5.68 +    val (results, thy) =
    5.69 +      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
    5.70      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    5.71  
    5.72      fun present () =