some markup for inlined files;
authorwenzelm
Fri Aug 24 13:05:14 2012 +0200 (2012-08-24 ago)
changeset 48919aaca64a7390c
parent 48918 6e5fd4585512
child 48920 9f84d872feba
some markup for inlined files;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Fri Aug 24 12:35:39 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Aug 24 13:05:14 2012 +0200
     1.3 @@ -64,23 +64,24 @@
     1.4  
     1.5  fun check_file dir file = File.check_file (File.full_path dir file);
     1.6  
     1.7 -fun make_file dir file =
     1.8 -  let val full_path = check_file dir file
     1.9 -  in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
    1.10 -
    1.11 -fun read_files cmd dir path =
    1.12 +fun read_files cmd dir (path, pos) =
    1.13    let
    1.14 +    fun make_file file =
    1.15 +      let
    1.16 +        val full_path = check_file dir file;
    1.17 +        val _ = Position.report pos (Isabelle_Markup.path (Path.implode full_path));
    1.18 +      in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
    1.19      val paths =
    1.20        (case Keyword.command_files cmd of
    1.21          [] => [path]
    1.22        | exts => map (fn ext => Path.ext ext path) exts);
    1.23 -  in map (make_file dir) paths end;
    1.24 +  in map make_file paths end;
    1.25  
    1.26  fun parse_files cmd =
    1.27    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
    1.28      (case Token.get_files tok of
    1.29        SOME files => files
    1.30 -    | NONE => read_files cmd (master_directory thy) (Path.explode name)));
    1.31 +    | NONE => read_files cmd (master_directory thy) (Path.explode name, Token.position_of tok)));
    1.32  
    1.33  local
    1.34  
    1.35 @@ -97,7 +98,7 @@
    1.36  fun find_file toks =
    1.37    rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    1.38      if Token.is_name tok then
    1.39 -      SOME (i, Path.explode (Token.content_of tok))
    1.40 +      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
    1.41          handle ERROR msg => error (msg ^ Token.pos_of tok)
    1.42      else NONE);
    1.43