From 20457cbff0b851ac9099847c91f74d48c5fe5be6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Apr 2015 15:47:52 +0200 Subject: CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch. --- ide/coqOps.ml | 30 +++++++++++------------------- ide/coqide.ml | 5 ----- ide/session.ml | 4 ---- ide/tags.ml | 5 ----- ide/tags.mli | 3 --- 5 files changed, 11 insertions(+), 36 deletions(-) (limited to 'ide') 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..eb994fe8e8 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1339,11 +1339,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/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 : -- cgit v1.2.3 From b667f6fec675d3a05ba0475bdb84beaeed7622ac Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 3 Apr 2015 08:48:30 +0200 Subject: Use the directory of the current session for selecting files to open. The old behavior was extremely annoying, especially when using coqide from the command line, since the "open" box would then point to a seemingly random point of the filesystem rather than to the directory of the files currently being edited (since they were passed on the command line rather than by point-and-click). The new behavior matches the one of mainstream editors, e.g. emacs, gedit. --- ide/coqide.ml | 7 +++++-- ide/ideutils.ml | 24 +++++++++++++----------- ide/ideutils.mli | 2 +- 3 files changed, 19 insertions(+), 14 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index eb994fe8e8..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 = 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 -- cgit v1.2.3 From b23edffbb4c0f57a5988c3ae218987f15e215097 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sun, 15 Feb 2015 13:54:59 -0500 Subject: Add extraction to JSON. This patch allows Coq terms to be extracted into the widely used JSON format. This is useful in at least two cases: - One might want to manipulate Coq values outside of Coq, but without being forced to use one of the three existing extraction languages (OCaml, Haskell, or Scheme), and without having to compile Coq's extracted result. This is especially useful when a Coq evaluation produces some data structure that needs to be moved out of Coq. Having to invoke an OCaml/Haskell/Scheme compiler just to get a data structure out of Coq is somewhat awkward. - One might want to experiment with extracting Coq code into other languages (Go, Javascript, etc), without having to write the whole extraction logic in OCaml and recompile Coq's extraction plugin each time. This makes it easy to quickly prototype extraction in any language, without having to build Coq from source. Extraction to JSON is implemented by adding the JSON "pseudo-language" to the extraction facility. Thus, one can extract the JSON encoding of a single term using: Extraction Language JSON. Extraction qualid. and extract an entire Coq library "ident" into "ident.json" using: Extraction Language JSON. Extraction Library ident. Nota (Pierre Letouzey) : this is an updated version of the original PullRequest, updated to match recent changes in trunk --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') 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 @@ (\%{locality}|(Reserved|Tactic)\%{space})?Notation \%{locality}Infix Declare\%{space}ML\%{space}Module - Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme) + Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON) \%{locality}Hint\%{space} -- cgit v1.2.3