tuned signature;
authorwenzelm
Sat Nov 16 18:08:57 2013 +0100 (2013-11-16 ago)
changeset 54451459cf6ee254e
parent 54450 7815563f50dc
child 54452 f3090621446e
tuned signature;
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:52:01 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 18:08:57 2013 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    val master_directory: theory -> Path.T
     1.5    val imports_of: theory -> (string * Position.T) list
     1.6    val thy_path: Path.T -> Path.T
     1.7 +  val read_files: Path.T -> string -> Path.T * Position.T -> Token.file list
     1.8    val parse_files: string -> (theory -> Token.file list) parser
     1.9    val check_thy: Path.T -> string ->
    1.10     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    1.11 @@ -55,11 +56,11 @@
    1.12  fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
    1.13  
    1.14  
    1.15 -(* inlined files *)
    1.16 +(* auxiliary files *)
    1.17  
    1.18  fun check_file dir file = File.check_file (File.full_path dir file);
    1.19  
    1.20 -fun read_files cmd dir (path, pos) =
    1.21 +fun read_files dir cmd (path, pos) =
    1.22    let
    1.23      fun make_file file =
    1.24        let
    1.25 @@ -76,48 +77,10 @@
    1.26    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
    1.27      (case Token.get_files tok of
    1.28        SOME files => files
    1.29 -    | NONE => read_files cmd (master_directory thy) (Path.explode name, Token.position_of tok)));
    1.30 -
    1.31 -local
    1.32 -
    1.33 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
    1.34 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    1.35 -      else (i1, t1) :: clean ((i2, t2) :: toks)
    1.36 -  | clean toks = toks;
    1.37 -
    1.38 -fun clean_tokens toks =
    1.39 -  ((0 upto length toks - 1) ~~ toks)
    1.40 -  |> filter (fn (_, tok) => Token.is_proper tok)
    1.41 -  |> clean;
    1.42 -
    1.43 -fun find_file toks =
    1.44 -  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    1.45 -    if Token.is_name tok then
    1.46 -      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
    1.47 -        handle ERROR msg => error (msg ^ Token.pos_of tok)
    1.48 -    else NONE);
    1.49 -
    1.50 -in
    1.51 -
    1.52 -fun resolve_files master_dir span =
    1.53 -  (case span of
    1.54 -    Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
    1.55 -      if Keyword.is_theory_load cmd then
    1.56 -        (case find_file toks of
    1.57 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    1.58 -        | SOME (i, path) =>
    1.59 -            let
    1.60 -              val toks' = toks |> map_index (fn (j, tok) =>
    1.61 -                if i = j then Token.put_files (read_files cmd master_dir path) tok
    1.62 -                else tok);
    1.63 -            in Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks') end)
    1.64 -      else span
    1.65 -  | span => span);
    1.66 -
    1.67 -end;
    1.68 +    | NONE => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)));
    1.69  
    1.70  
    1.71 -(* check files *)
    1.72 +(* theory files *)
    1.73  
    1.74  val thy_path = Path.ext "thy";
    1.75  
    1.76 @@ -213,7 +176,7 @@
    1.77      val lexs = Keyword.get_lexicons ();
    1.78  
    1.79      val toks = Thy_Syntax.parse_tokens lexs text_pos text;
    1.80 -    val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
    1.81 +    val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
    1.82      val elements = Thy_Syntax.parse_elements spans;
    1.83  
    1.84      val _ = Present.theory_source name
     2.1 --- a/src/Pure/Thy/thy_syntax.ML	Sat Nov 16 17:52:01 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sat Nov 16 18:08:57 2013 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4    val span_content: span -> Token.T list
     2.5    val present_span: span -> Output.output
     2.6    val parse_spans: Token.T list -> span list
     2.7 +  val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
     2.8    datatype 'a element = Element of 'a * ('a element list * 'a) option
     2.9    val atom: 'a -> 'a element
    2.10    val map_element: ('a -> 'b) -> 'a element -> 'b element
    2.11 @@ -142,6 +143,47 @@
    2.12  end;
    2.13  
    2.14  
    2.15 +(* inlined files *)
    2.16 +
    2.17 +local
    2.18 +
    2.19 +fun clean ((i1, t1) :: (i2, t2) :: toks) =
    2.20 +      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    2.21 +      else (i1, t1) :: clean ((i2, t2) :: toks)
    2.22 +  | clean toks = toks;
    2.23 +
    2.24 +fun clean_tokens toks =
    2.25 +  ((0 upto length toks - 1) ~~ toks)
    2.26 +  |> filter (fn (_, tok) => Token.is_proper tok)
    2.27 +  |> clean;
    2.28 +
    2.29 +fun find_file toks =
    2.30 +  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    2.31 +    if Token.is_name tok then
    2.32 +      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
    2.33 +        handle ERROR msg => error (msg ^ Token.pos_of tok)
    2.34 +    else NONE);
    2.35 +
    2.36 +in
    2.37 +
    2.38 +fun resolve_files read_files span =
    2.39 +  (case span of
    2.40 +    Span (Command (cmd, pos), toks) =>
    2.41 +      if Keyword.is_theory_load cmd then
    2.42 +        (case find_file toks of
    2.43 +          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    2.44 +        | SOME (i, path) =>
    2.45 +            let
    2.46 +              val toks' = toks |> map_index (fn (j, tok) =>
    2.47 +                if i = j then Token.put_files (read_files cmd path) tok
    2.48 +                else tok);
    2.49 +            in Span (Command (cmd, pos), toks') end)
    2.50 +      else span
    2.51 +  | _ => span);
    2.52 +
    2.53 +end;
    2.54 +
    2.55 +
    2.56  
    2.57  (** specification elements: commands with optional proof **)
    2.58