products/Sources/formale Sprachen/Coq/ide image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fileOps.ml   Sprache: SML

Original von: Coq©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Ideutils

let revert_timer = mktimer ()
let autosave_timer = mktimer ()

class type ops =
object
  method filename : string option
  method update_stats : unit
  method changed_on_disk : bool
  method revert : ?parent:GWindow.window -> unit -> unit
  method auto_save : unit
  method save : string -> bool
  method saveas : ?parent:GWindow.window -> string -> bool
end

class fileops (buffer:GText.buffer) _fn (reset_handler:unit->unit) =
object(self)

  val mutable filename = _fn
  val mutable last_stats = NoSuchFile
  val mutable last_modification_time = 0.
  val mutable last_auto_save_time = 0.

  method filename = filename

  method update_stats = match filename with
    |Some f -> last_stats <- Ideutils.stat f
    |_ -> ()

  method changed_on_disk = match filename with
    |None -> false
    |Some f -> match Ideutils.stat f, last_stats with
        |MTime cur_mt, MTime last_mt -> cur_mt > last_mt
        |MTime _, (NoSuchFile|OtherError) -> true
        |NoSuchFile, MTime _ ->
          flash_info ("Warning, file not on disk anymore : "^f);
          false
        |_ -> false

  method revert ?parent () =
    let do_revert f =
      push_info "Reverting buffer";
      try
        reset_handler ();
        let b = Buffer.create 1024 in
        Ideutils.read_file f b;
        let s = try_convert (Buffer.contents b) in
        buffer#set_text s;
        self#update_stats;
        buffer#place_cursor ~where:buffer#start_iter;
        buffer#set_modified false;
        pop_info ();
        flash_info "Buffer reverted";
        Sentence.tag_all buffer;
      with _  ->
        pop_info ();
        flash_info "Warning: could not revert buffer";
    in
    match filename with
      | None -> ()
      | Some f ->
        if not buffer#modified then do_revert f
        else
          let answ = Configwin_ihm.question_box
            ~title:"Modified buffer changed on disk"
            ~buttons:["Revert from File";
                      "Overwrite File";
                      "Disable Auto Revert"]
            ~default:0
            ~icon:(stock_to_widget `DIALOG_WARNING)
            ?parent
            "Some unsaved buffers changed on disk"
          in
          match answ with
            | 1 -> do_revert f
            | 2 -> if self#save f then flash_info "Overwritten" else
                flash_info "Could not overwrite file"
            | _ ->
              Minilib.log "Auto revert set to false";
              Preferences.global_auto_revert#set false;
              revert_timer.kill ()

  method save f =
    if try_export f (buffer#get_text ()) then begin
      filename <- Some f;
      self#update_stats;
      buffer#set_modified false;
      (match self#auto_save_name with
        | None -> ()
        | Some fn -> try Sys.remove fn with _ -> ());
      true
    end
    else false

  method saveas ?parent f =
  if not (Sys.file_exists f) then self#save f
  else
    let answ = Configwin_ihm.question_box ~title:"File exists on disk"
      ~buttons:["Overwrite""Cancel";]
      ~default:1
      ~icon:(warn_image ())#coerce
      ?parent
      ("File "^f^" already exists")
    in
    match answ with
      | 1 -> self#save f
      | _ -> false

  method private auto_save_name =
    match filename with
      | None -> None
      | Some f ->
        let dir = Filename.dirname f in
        let base = (fst Preferences.auto_save_name#get) ^
          (Filename.basename f) ^
          (snd Preferences.auto_save_name#get)
        in Some (Filename.concat dir base)

  method private need_auto_save =
    buffer#modified &&
      last_modification_time > last_auto_save_time

  method auto_save =
    if self#need_auto_save then begin
      match self#auto_save_name with
        | None -> ()
        | Some fn ->
          try
            last_auto_save_time <- Unix.time();
            Minilib.log ("Autosave time: "^(string_of_float (Unix.time())));
            if try_export fn (buffer#get_text ()) then begin
              flash_info ~delay:1000 "Autosaved"
            end
            else warning
              ("Autosave failed (check if " ^ fn ^ " is writable)")
          with _ ->
            warning ("Autosave: unexpected error while writing "^fn)
    end

  initializer
  let _ = buffer#connect#end_user_action
    ~callback:(fun () -> last_modification_time <- Unix.time ())
  in ()

end

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff