Merge branch 'v8.5' into trunk

8 files changed, 31 insertions, 51 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index 38dabda506..65150d6a95 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -164,7 +164,7 @@
 	  <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
 	  <keyword>\%{locality}Infix</keyword>
 	  <keyword>Declare\%{space}ML\%{space}Module</keyword>
-	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword>
+	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
 	</context>
 	<context id="hint-command" style-ref="vernac-keyword">
 	  <prefix>\%{locality}Hint\%{space}</prefix>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c6073d599d..af728471f7 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -276,21 +276,11 @@ object(self)
     Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
     self#print_stack;
     let qed_s = Doc.tip_data document in
-    buffer#apply_tag Tags.Script.read_only
-      ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char
-        (fun c -> not(Glib.Unichar.isspace c)))
-      ~stop:(buffer#get_iter_at_mark qed_s.stop);
     buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
       (`NAME "stop_of_input")
 
   method private exit_focus =
     Minilib.log "Unfocusing";
-    begin try
-      let { start; stop } = Doc.tip_data document in
-      buffer#remove_tag Tags.Script.read_only
-        ~start:(buffer#get_iter_at_mark start)
-        ~stop:(buffer#get_iter_at_mark stop)
-    with Doc.Empty -> () end;
     Doc.unfocus document;
     self#print_stack;
     begin try
@@ -515,7 +505,7 @@ object(self)
       | Some (start, stop) ->
         if until n start stop then begin
           ()
-        end else if start#has_tag Tags.Script.processed then begin
+        end else if stop#backward_char#has_tag Tags.Script.processed then begin
           Queue.push (`Skip (start, stop)) queue;
           loop n stop
         end else begin
@@ -563,12 +553,15 @@ object(self)
       script#recenter_insert;
       match topstack with
       | [] -> self#show_goals_aux ?move_insert ()
-      | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
+      | (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
     let process_queue queue =
       let rec loop tip topstack =
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
-        | `Skip(start,stop), [] -> assert false
+        | `Skip(start,stop), [] ->
+            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            self#discard_command_queue queue;
+            conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -589,7 +582,7 @@ object(self)
                   Doc.assign_tip_id document id;
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
-                  self#cleanup ~all:true (Doc.cut_at document tip);
+                  self#cleanup (Doc.cut_at document tip);
                   logger Pp.Notice msg;
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
@@ -651,7 +644,7 @@ object(self)
       Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
     with Not_found -> initial_state, Doc.focused document 
 
-  method private cleanup ~all seg =
+  method private cleanup seg =
     if seg <> [] then begin
       let start = buffer#get_iter_at_mark (CList.last seg).start in
       let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
@@ -662,7 +655,6 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      if all then buffer#remove_tag Tags.Script.read_only ~start ~stop;
       buffer#remove_tag Tags.Script.error ~start ~stop;
       buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
@@ -694,13 +686,13 @@ object(self)
       Coq.bind (Coq.edit_at to_id) (function
       | Good (CSig.Inl (* NewTip *) ()) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup ~all:true (Doc.cut_at document to_id);
+          self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Good (CSig.Inr (* Focus  *) (stop_id,(start_id,tip))) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup ~all:true (Doc.cut_at document tip);
+          self#cleanup (Doc.cut_at document tip);
           self#enter_focus start_id stop_id;
-          self#cleanup ~all:false (Doc.cut_at document to_id);
+          self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Pp.Error "Fixme LOC";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 87efd17d22..0f4cb7b073 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -253,11 +253,14 @@ let newfile _ =
   !refresh_editor_hook ();
   notebook#goto_page index
 
-let load _ =
-  match select_file_for_open ~title:"Load file" () with
+let load sn =
+  let filename = sn.fileops#filename in
+  match select_file_for_open ~title:"Load file" ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
+let load = cb_on_current_term load
+
 let save _ = on_current_term (FileAux.check_save ~saveas:false)
 
 let saveas sn =
@@ -1339,11 +1342,6 @@ let build_ui () =
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
   Tags.Script.incomplete#set_property
     (`BACKGROUND_GDK (Tags.get_processed_color ())); 
-  Tags.Script.read_only#set_property
-    (`BACKGROUND_STIPPLE
-      (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
-  Tags.Script.read_only#set_property
-    (`BACKGROUND_GDK (Tags.get_processed_color ())); 
 
   (* Showtime ! *)
   w#show ()
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 973ff0b778..67e4bdb0c9 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -144,8 +144,7 @@ let current_dir () = match current.project_path with
 | None -> ""
 | Some dir -> dir
 
-let select_file_for_open ~title () =
-  let file = ref None in
+let select_file_for_open ~title ?filename () =
   let file_chooser =
     GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
   in
@@ -154,19 +153,22 @@ let select_file_for_open ~title () =
   file_chooser#add_filter (filter_coq_files ());
   file_chooser#add_filter (filter_all_files ());
   file_chooser#set_default_response `OPEN;
-  ignore (file_chooser#set_current_folder (current_dir ()));
-  begin match file_chooser#run () with
+  let dir = match filename with
+    | None -> current_dir ()
+    | Some f -> Filename.dirname f in
+  ignore (file_chooser#set_current_folder dir);
+  let file =
+    match file_chooser#run () with
     | `OPEN ->
       begin
-	file := file_chooser#filename;
-	match !file with
-	  | None -> ()
-	  | Some s -> current.project_path <- file_chooser#current_folder
+	match file_chooser#filename with
+	  | None -> None
+	  | Some _ as f ->
+            current.project_path <- file_chooser#current_folder; f
       end
-    | `DELETE_EVENT | `CANCEL -> ()
-  end ;
+    | `DELETE_EVENT | `CANCEL -> None in
   file_chooser#destroy ();
-  !file
+  file
 
 let select_file_for_save ~title ?filename () =
   let file = ref None in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index c2b51dd396..1fb30e4d72 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
 val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 
-val select_file_for_open : title:string -> unit -> string option
+val select_file_for_open : title:string -> ?filename:string -> unit -> string option
 val select_file_for_save :
   title:string -> ?filename:string -> unit -> string option
 val try_convert : string -> string
diff --git a/ide/session.ml b/ide/session.ml
index e0466b7e3a..12b7796633 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -156,8 +156,6 @@ let set_buffer_handlers
     let () = update_prev it in
     if it#has_tag Tags.Script.to_process then
       cancel_signal "Altering the script being processed in not implemented"
-    else if it#has_tag Tags.Script.read_only then
-      cancel_signal "Altering read_only text not allowed"
     else if it#has_tag Tags.Script.processed then
       call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
     else if it#has_tag Tags.Script.error_bg then begin
@@ -175,8 +173,6 @@ let set_buffer_handlers
       if min_iter#equal max_iter then ()
       else if min_iter#has_tag Tags.Script.to_process then
         cancel_signal "Altering the script being processed in not implemented"
-      else if min_iter#has_tag Tags.Script.read_only then
-        cancel_signal "Altering read_only text not allowed"
       else if min_iter#has_tag Tags.Script.processed then
         call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
       else if min_iter#has_tag Tags.Script.error_bg then
diff --git a/ide/tags.ml b/ide/tags.ml
index d4460b0770..c9b57af4cb 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -52,10 +52,6 @@ struct
     t
   let all = edit_zone :: all
   
-  let read_only = make_tag table ~name:"read_only" [`EDITABLE false;
-          `BACKGROUND !processing_color;
-          `BACKGROUND_STIPPLE_SET true ]
-
 end
 module Proof =
 struct
@@ -96,7 +92,6 @@ let set_processing_color clr =
   let s = string_of_color clr in
   processing_color := s;
   Script.incomplete#set_property (`BACKGROUND s);
-  Script.read_only#set_property (`BACKGROUND s);
   Script.to_process#set_property (`BACKGROUND s)
 
 let get_error_color () = color_of_string !error_color
diff --git a/ide/tags.mli b/ide/tags.mli
index e68015c991..14cfd0dbfe 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -21,9 +21,6 @@ sig
   val tooltip : GText.tag
   val edit_zone : GText.tag (* for debugging *)
   val all : GText.tag list
-
-  (* Not part of the all list. Special tags! *)
-  val read_only : GText.tag
 end
 
 module Proof :