src/Pure/PIDE/document.ML
changeset 47335 693276dcc512
parent 47051 b32e6de4a39b
child 47336 bed4b2738d8a
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 04 10:38:04 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 04 14:00:47 2012 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  
     1.5  abstype state = State of
     1.6   {versions: version Inttab.table,  (*version_id -> document content*)
     1.7 -  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> name * span*)
     1.8 +  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
     1.9    execution: version_id * Future.group}  (*current execution process*)
    1.10  with
    1.11  
    1.12 @@ -310,6 +310,12 @@
    1.13  
    1.14  local
    1.15  
    1.16 +fun run int tr st =
    1.17 +  (case Toplevel.transition int tr st of
    1.18 +    SOME (st', NONE) => ([], SOME st')
    1.19 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    1.20 +  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    1.21 +
    1.22  fun timing tr t =
    1.23    if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
    1.24  
    1.25 @@ -322,12 +328,6 @@
    1.26    (Lazy.lazy o Toplevel.setmp_thread_position tr)
    1.27      (fn () => Toplevel.print_state false st);
    1.28  
    1.29 -fun run int tr st =
    1.30 -  (case Toplevel.transition int tr st of
    1.31 -    SOME (st', NONE) => ([], SOME st')
    1.32 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    1.33 -  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    1.34 -
    1.35  in
    1.36  
    1.37  fun run_command tr st =
    1.38 @@ -363,7 +363,6 @@
    1.39  
    1.40  
    1.41  
    1.42 -
    1.43  (** update **)
    1.44  
    1.45  (* perspective *)
    1.46 @@ -380,6 +379,37 @@
    1.47  
    1.48  local
    1.49  
    1.50 +fun make_required nodes =
    1.51 +  let
    1.52 +    val all_visible =
    1.53 +      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
    1.54 +      |> Graph.all_preds nodes;
    1.55 +    val required =
    1.56 +      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
    1.57 +        all_visible Symtab.empty;
    1.58 +  in Symtab.defined required end;
    1.59 +
    1.60 +fun init_theory deps node =
    1.61 +  let
    1.62 +    (* FIXME provide files via Scala layer, not master_dir *)
    1.63 +    val (dir, header) = Exn.release (get_header node);
    1.64 +    val master_dir =
    1.65 +      (case Url.explode dir of
    1.66 +        Url.File path => path
    1.67 +      | _ => Path.current);
    1.68 +    val parents =
    1.69 +      #imports header |> map (fn import =>
    1.70 +        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.71 +          SOME thy => thy
    1.72 +        | NONE =>
    1.73 +            get_theory (Position.file_only import)
    1.74 +              (snd (Future.join (the (AList.lookup (op =) deps import))))));
    1.75 +  in Thy_Load.begin_theory master_dir header parents end;
    1.76 +
    1.77 +fun check_theory nodes name =
    1.78 +  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
    1.79 +  is_some (Exn.get_res (get_header (get_node nodes name)));
    1.80 +
    1.81  fun last_common state last_visible node0 node =
    1.82    let
    1.83      fun update_flags prev (visible, initial) =
    1.84 @@ -428,37 +458,6 @@
    1.85        val command_exec' = (command_id', (exec_id', exec'));
    1.86      in SOME (command_exec' :: execs, command_exec', init') end;
    1.87  
    1.88 -fun make_required nodes =
    1.89 -  let
    1.90 -    val all_visible =
    1.91 -      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
    1.92 -      |> Graph.all_preds nodes;
    1.93 -    val required =
    1.94 -      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
    1.95 -        all_visible Symtab.empty;
    1.96 -  in Symtab.defined required end;
    1.97 -
    1.98 -fun check_theory nodes name =
    1.99 -  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
   1.100 -  is_some (Exn.get_res (get_header (get_node nodes name)));
   1.101 -
   1.102 -fun init_theory deps node =
   1.103 -  let
   1.104 -    (* FIXME provide files via Scala layer, not master_dir *)
   1.105 -    val (dir, header) = Exn.release (get_header node);
   1.106 -    val master_dir =
   1.107 -      (case Url.explode dir of
   1.108 -        Url.File path => path
   1.109 -      | _ => Path.current);
   1.110 -    val parents =
   1.111 -      #imports header |> map (fn import =>
   1.112 -        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
   1.113 -          SOME thy => thy
   1.114 -        | NONE =>
   1.115 -            get_theory (Position.file_only import)
   1.116 -              (snd (Future.join (the (AList.lookup (op =) deps import))))));
   1.117 -  in Thy_Load.begin_theory master_dir header parents end;
   1.118 -
   1.119  in
   1.120  
   1.121  fun update (old_id: version_id) (new_id: version_id) edits state =