more uniform handling of inlined files;
authorwenzelm
Tue Nov 19 21:49:31 2013 +0100 (2013-11-19 ago)
changeset 5452311087efad95e
parent 54522 761be40990f1
child 54524 14609d36cab8
more uniform handling of inlined files;
src/Pure/Isar/keyword.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/keyword.ML	Tue Nov 19 20:59:05 2013 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Tue Nov 19 21:49:31 2013 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     1.5    val is_keyword: string -> bool
     1.6    val command_keyword: string -> T option
     1.7 -  val command_files: string -> string list
     1.8 +  val command_files: string -> Path.T -> Path.T list
     1.9    val command_tags: string -> string list
    1.10    val dest: unit -> string list * string list
    1.11    val define: string * T option -> unit
    1.12 @@ -196,7 +196,15 @@
    1.13    in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    1.14  
    1.15  fun command_keyword name = Symtab.lookup (get_commands ()) name;
    1.16 -val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
    1.17 +
    1.18 +fun command_files name path =
    1.19 +  (case command_keyword name of
    1.20 +    NONE => []
    1.21 +  | SOME (Keyword {kind, files, ...}) =>
    1.22 +      if kind <> kind_of thy_load then []
    1.23 +      else if null files then [path]
    1.24 +      else map (fn ext => Path.ext ext path) files);
    1.25 +
    1.26  val command_tags = these o Option.map tags_of o command_keyword;
    1.27  
    1.28  fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Nov 19 20:59:05 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Nov 19 21:49:31 2013 +0100
     2.3 @@ -88,10 +88,20 @@
     2.4  fun resolve_files blobs toks =
     2.5    (case Thy_Syntax.parse_spans toks of
     2.6      [span] => span
     2.7 -      |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
     2.8 -        blobs |> (map o Exn.map_result) (fn (file, text) =>
     2.9 -          let val _ = Position.report pos (Markup.path file);
    2.10 -          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
    2.11 +      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    2.12 +        let
    2.13 +          fun make_file src_path (Exn.Res (file, text)) =
    2.14 +                let val _ = Position.report pos (Markup.path file);
    2.15 +                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
    2.16 +            | make_file _ (Exn.Exn e) = Exn.Exn e;
    2.17 +
    2.18 +          val src_paths = Keyword.command_files cmd path;
    2.19 +        in
    2.20 +          if null blobs then []
    2.21 +          else if length src_paths <> length blobs then
    2.22 +            error ("Misalignment of inlined files" ^ Position.here pos)
    2.23 +          else map2 make_file src_paths blobs
    2.24 +        end)
    2.25        |> Thy_Syntax.span_content
    2.26    | _ => toks);
    2.27  
     3.1 --- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 20:59:05 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Nov 19 21:49:31 2013 +0100
     3.3 @@ -61,16 +61,12 @@
     3.4  
     3.5  fun read_files dir cmd (path, pos) =
     3.6    let
     3.7 -    fun make_file file =
     3.8 +    fun make_file src_path =
     3.9        let
    3.10 -        val _ = Position.report pos (Markup.path (Path.implode file));
    3.11 -        val full_path = check_file dir file;
    3.12 -      in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
    3.13 -    val paths =
    3.14 -      (case Keyword.command_files cmd of
    3.15 -        [] => [path]
    3.16 -      | exts => map (fn ext => Path.ext ext path) exts);
    3.17 -  in map make_file paths end;
    3.18 +        val full_path = check_file dir src_path;
    3.19 +        val _ = Position.report pos (Markup.path (Path.implode full_path));
    3.20 +      in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
    3.21 +  in map make_file (Keyword.command_files cmd path) end;
    3.22  
    3.23  fun parse_files cmd =
    3.24    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>