more precises positions;
authorwenzelm
Mon Mar 16 14:15:15 2015 +0100 (2015-03-16)
changeset 597168c56b34a88b0
parent 59715 4f0d0e4ad68d
child 59717 44a3ed0b8265
more precises positions;
more permissive imports;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Mar 16 13:32:31 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Mar 16 14:15:15 2015 +0100
     1.3 @@ -520,16 +520,24 @@
     1.4      val master_dir = master_directory node;
     1.5      val header = read_header node span;
     1.6      val imports = #imports header;
     1.7 -    val parents =
     1.8 -      imports |> map (fn (import, _) =>
     1.9 +
    1.10 +    fun maybe_end_theory pos st =
    1.11 +      SOME (Toplevel.end_theory pos st)
    1.12 +        handle ERROR msg => (Output.error_message msg; NONE);
    1.13 +    val parents_reports =
    1.14 +      imports |> map_filter (fn (import, pos) =>
    1.15          (case loaded_theory import of
    1.16 -          SOME thy => thy
    1.17 -        | NONE =>
    1.18 -            Toplevel.end_theory (Position.file_only import)
    1.19 +          NONE =>
    1.20 +            maybe_end_theory pos
    1.21                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    1.22                  NONE => Toplevel.toplevel
    1.23 -              | SOME eval => Command.eval_result_state eval)));
    1.24 -    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    1.25 +              | SOME eval => Command.eval_result_state eval)
    1.26 +        | some => some)
    1.27 +        |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
    1.28 +
    1.29 +    val parents =
    1.30 +      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
    1.31 +    val _ = Position.reports (map #2 parents_reports);
    1.32    in Resources.begin_theory master_dir header parents end;
    1.33  
    1.34  fun check_theory full name node =