diff -Nru prooftree-0.12/about_window.ml prooftree-0.13/about_window.ml --- prooftree-0.12/about_window.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/about_window.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: about_window.ml,v 1.6 2013/03/28 08:02:00 tews Exp $ + * $Id: about_window.ml,v 1.7 2016/01/23 12:57:13 tews Exp $ *) diff -Nru prooftree-0.12/ChangeLog prooftree-0.13/ChangeLog --- prooftree-0.12/ChangeLog 2013-05-17 13:00:54.000000000 +0000 +++ prooftree-0.13/ChangeLog 2017-01-03 10:35:43.000000000 +0000 @@ -1,3 +1,121 @@ +2017-01-03 Hendrik Tews + + * prepare changes.html for release + +2017-01-02 Hendrik Tews + + * compile with -safe-string + +2017-01-02 Hendrik Tews + + * update doc + +2016-12-28 Hendrik Tews + + * gitignore and some debugging code in comments + +2016-01-23 Hendrik Tews + + * update copyright + +2016-01-22 Hendrik Tews + + * add tests for cycle/swap/revgoals, Grab Existentials/Unshelve, giveup + +2016-01-21 Hendrik Tews + + * update evar parsing for 8.5 + +2016-01-18 Hendrik Tews + + * disable implicit optional argument elimination warning 48 + +2016-01-18 Hendrik Tews + + * fix deprecated or + +2016-01-17 Hendrik Tews + + * fix 4.02 compilation problem + +2016-01-16 Hendrik Tews + + * crash fix ?? + +2013-08-11 Hendrik Tews + + * rename delete_non_sticky_node_window + +2013-08-10 Hendrik Tews + + * let the cancel button reset the configuration + +2013-08-10 Hendrik Tews + + * display a warning for config file version errors + +2013-08-10 Hendrik Tews + + * catch input log file opening errors + +2013-08-08 Hendrik Tews + + * close old PG log file, before changing it + +2013-08-08 Hendrik Tews + + * update doc + +2013-08-08 Hendrik Tews + + * config window without apply + +2013-08-05 Hendrik Tews + + * use stock items for most buttons + +2013-08-04 Hendrik Tews + + * describe prooftree notification messages and other doc fixes + +2013-08-03 Hendrik Tews + + * show selected menu entry + +2013-08-03 Hendrik Tews + + * update INSTALL, README; add compatibility file + +2013-08-03 Hendrik Tews + + * update man page + +2013-08-02 Hendrik Tews + + * quit prooftree when closing -config or -help-dialog windows + * update help window text + +2013-08-01 Hendrik Tews + + * add history list in external sequent windows + +2013-07-23 Hendrik Tews + + * fix wrong existential info in external node windows + +2013-07-18 Hendrik Tews + + * fix title of orphaned node windows + * don't update content of sticky node windows + +2013-05-17 Hendrik Tews + + * release version 0.12 on 2013-05-17 13:39:12 UTC + +2013-05-17 Hendrik Tews + + * prepare changes.html for release + 2013-05-17 Hendrik Tews * prepare changes.html for release diff -Nru prooftree-0.12/changes.html prooftree-0.13/changes.html --- prooftree-0.12/changes.html 2013-05-17 13:00:54.000000000 +0000 +++ prooftree-0.13/changes.html 2017-01-03 10:35:43.000000000 +0000 @@ -37,6 +37,20 @@ --> +
2017-01-03: Prooftree 0.13 released +
+
    +
  • sequent history accessible in external sequent node windows +
    • +
  • new menu item Show selected +
    • +
  • improved configuration dialog +
    • +
  • support Coq 8.5 and 8.6 +

    • +
+ +
2013-05-17: Prooftree 0.12 released
    @@ -189,7 +203,7 @@
    last changed on -17 May 2013 + 2 Jan 2017 by Hendrik diff -Nru prooftree-0.12/compatibility prooftree-0.13/compatibility --- prooftree-0.12/compatibility 1970-01-01 00:00:00.000000000 +0000 +++ prooftree-0.13/compatibility 2017-01-03 10:35:43.000000000 +0000 @@ -0,0 +1,7 @@ +protocol prooftree Proof General + +3 0.11 >= 4.3pre130327 + +2 0.9 - 0.10 4.2; 4.2pre120110 - 4.3pre130111 + +1 0.8 4.2pre120104 \ No newline at end of file diff -Nru prooftree-0.12/configuration.ml prooftree-0.13/configuration.ml --- prooftree-0.12/configuration.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/configuration.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: configuration.ml,v 1.39 2013/03/28 08:02:00 tews Exp $ + * $Id: configuration.ml,v 1.46 2016/01/23 12:57:13 tews Exp $ *) @@ -417,20 +417,27 @@ let configuration_updated_callback = ref (fun () -> ()) +(** Update the configuration and all directly derived state variables. *) +let update_configuration_record c = + current_config := c; + update_font_and_color () + (** [update_configuration c] does all the necessary actions to make [c] the current configuration. It stores [c] in {!current_config}, updates the references for fonts and colors and calls all [configuration_updated] functions/methods. *) let update_configuration c = - current_config := c; - update_font_and_color (); + update_configuration_record c; !configuration_updated_callback () (** Reference for the argument of the [-geometry] option. *) let geometry_string = ref "" +(** Flag for option [-config]. *) +let start_config_dialog = ref false + (***************************************************************************** *****************************************************************************) @@ -468,9 +475,8 @@ *) let read_config_file file_name : t = let header_len = String.length config_file_header in - let header = String.create header_len in let ic = open_in_bin file_name in - really_input ic header 0 header_len; + let header = really_input_string ic header_len in if header = config_file_header then begin let c = (Marshal.from_channel ic : t) in @@ -483,18 +489,33 @@ (** Try to load the configuration file at {!config_file_location}, ignoring all errors. If a valid configuration file is found, the - current configuration is updated. Used during start-up. + current configuration record is updated. If an incompatible + version is found, a warning message is displayed. Used during + start-up. *) let try_load_config_file () = let copt = try - Some(read_config_file config_file_location) + (* print_endline "before read"; *) + let res = Some(read_config_file config_file_location) in + (* print_endline "after read"; *) + res with - | _ -> None + | Failure "Incompatible configuration file version" -> + print_endline "version error"; + run_message_dialog + ("File " ^ config_file_location ^ + " is not compatible with this version of Prooftree!\n\ + Using default configuration.") + `WARNING; + None + | _ -> + print_endline "other error"; + None in match copt with | None -> () - | Some c -> update_configuration c + | Some c -> update_configuration_record c (***************************************************************************** @@ -514,23 +535,24 @@ set up by the function that creates objects. Arguments are + - old_config current config at config window start time - top_window {xref lablgtk class GWindow.window} of the top-level widget - - line_width_spinner {xref lablgtk class GEdit.spin_button} + - line_width_adjustment {xref lablgtk class GData.adjustment} for line width - - turnstile_size_spinner {xref lablgtk class GEdit.spin_button} + - turnstile_size_adjustment {xref lablgtk class GData.adjustment} for turnstile size - - line_sep_spinner {xref lablgtk class GEdit.spin_button} + - line_sep_adjustment {xref lablgtk class GData.adjustment} for line gap - - proof_tree_sep_spinner {xref lablgtk class GEdit.spin_button} + - proof_tree_sep_adjustment {xref lablgtk class GData.adjustment} for proof tree sep - - subtree_sep_spinner {xref lablgtk class GEdit.spin_button} + - subtree_sep_adjustment {xref lablgtk class GData.adjustment} for node padding - - command_length_spinner {xref lablgtk class GEdit.spin_button} + - command_length_adjustment {xref lablgtk class GData.adjustment} for command length - - level_dist_spinner {xref lablgtk class GEdit.spin_button} + - level_dist_adjustment {xref lablgtk class GData.adjustment} for vertical distance - - layer_sep_spinner {xref lablgtk class GEdit.spin_button} + - layer_sep_adjustment {xref lablgtk class GData.adjustment} layer sep - tree_font_button {xref lablgtk class GButton.font_button} for proof tree font @@ -550,7 +572,7 @@ for create exist. - ext_inst_color_button {xref lablgtk class GButton.color_button} for instant. exist. - - drag_accel_spinner {xref lablgtk class GEdit.spin_button} + - drag_accel_adjustment {xref lablgtk class GData.adjustment} for drac acceleration - doc_tooltip_check_box {xref lablgtk class GButton.toggle_button} for the help tool-tips check bock @@ -558,41 +580,37 @@ for the turnstile tool-tips check bock - command_tooltip_check_box {xref lablgtk class GButton.toggle_button} for the command tool-tips check bock - - default_size_width_spinner {xref lablgtk class GEdit.spin_button} + - default_size_width_adjustment {xref lablgtk class GData.adjustment} for default window size width - - default_size_height_spinner {xref lablgtk class GEdit.spin_button} + - default_size_height_adjustment {xref lablgtk class GData.adjustment} for default window size height - - internal_seq_lines_spinner {xref lablgtk class GEdit.spin_button} + - internal_seq_lines_adjustment {xref lablgtk class GData.adjustment} for lines in the internal sequent window - - external_node_lines_spinner {xref lablgtk class GEdit.spin_button} + - external_node_lines_adjustment {xref lablgtk class GData.adjustment} for lines in external node windows - - ext_table_lines_spinner {xref lablgtk class GEdit.spin_button} + - ext_table_lines_adjustment {xref lablgtk class GData.adjustment} for lines in evar table - debug_check_box {xref lablgtk class GButton.toggle_button} for the more-debug-info check box - tee_file_box_check_box {xref lablgtk class GButton.toggle_button} for log-input check box - - tee_file_name_label {xref lablgtk class GMisc.label} - of the log-file label - tee_file_name_entry {xref lablgtk class GEdit.entry} of the log-file text entry - - tee_file_name_button {xref lablgtk class GButton.button} - of the log-file button that - starts the file selection dialog - tooltip_misc_objects list of {xref lablgtk class GObj.misc_ops} of config dialog elements that have a tool-tip to switch on and off *) -class config_window +class config_window + old_config top_window - line_width_spinner - turnstile_size_spinner - line_sep_spinner - proof_tree_sep_spinner - subtree_sep_spinner - command_length_spinner - level_dist_spinner - layer_sep_spinner + line_width_adjustment + turnstile_size_adjustment + line_sep_adjustment + proof_tree_sep_adjustment + subtree_sep_adjustment + command_length_adjustment + level_dist_adjustment + layer_sep_adjustment tree_font_button sequent_font_button current_color_button @@ -603,86 +621,31 @@ (* mark_subtree_color_button *) ext_create_color_button ext_inst_color_button - drag_accel_spinner + drag_accel_adjustment doc_tooltip_check_box turnstile_tooltip_check_box command_tooltip_check_box - default_size_width_spinner default_size_height_spinner - internal_seq_lines_spinner - external_node_lines_spinner - ext_table_lines_spinner + default_size_width_adjustment default_size_height_adjustment + internal_seq_lines_adjustment + external_node_lines_adjustment + ext_table_lines_adjustment debug_check_box tee_file_box_check_box - tee_file_name_label tee_file_name_entry tee_file_name_button + tee_file_name_entry tooltip_misc_objects = object (self) - (** {xref lablgtk class GData.adjustment} of the line-width spin button. *) - val line_width_adjustment = line_width_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the turnstile-size spin - button. - *) - val turnstile_size_adjustment = turnstile_size_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the line-gap spin button. *) - val line_sep_adjustment = line_sep_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the proof_tree_sep spin - button. - *) - val proof_tree_sep_adjustment = proof_tree_sep_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the node-padding spin - button. - *) - val subtree_sep_adjustment = subtree_sep_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the command-length spin - button. - *) - val command_length_adjustment = command_length_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the vertical-distance - spin button. - *) - val level_dist_adjustment = level_dist_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the layer_sep spin - button. + (** The callbacks for the configuration update may trigger several + config updates in a row. When this setting is [true], then the + config update is not done. *) - val layer_sep_adjustment = layer_sep_spinner#adjustment + val mutable delay_config_update = false - (** {xref lablgtk class GData.adjustment} of the drag-acceleration - spin button. + (** Set to [true] when the log-file chooser dialog sets the log-file + name to avoid switching off the log file check box. *) - val drag_accel_adjustment = drag_accel_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the - default-window-size-width spin button. - *) - val default_size_width_adjustment = default_size_width_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the - default-window-size-height spin button. - *) - val default_size_height_adjustment = default_size_height_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the spin button for the - number of lines in the internal sequent window. - *) - val internal_seq_lines_adjustment = internal_seq_lines_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the spin button for the - number of lines in external node windows. - *) - val external_node_lines_adjustment = external_node_lines_spinner#adjustment - - (** {xref lablgtk class GData.adjustment} of the spin button for the - default number of lines in the existential variable table. - *) - val ext_table_lines_adjustment = ext_table_lines_spinner#adjustment + val mutable clean_tee_file_check_box = true (** Make this configuration dialog visible. *) method present = top_window#present() @@ -691,6 +654,7 @@ configuration of the configuration record [c]. *) method set_configuration conf = + (* print_endline "set config start"; *) line_width_adjustment#set_value (float_of_int conf.turnstile_line_width); turnstile_size_adjustment#set_value (float_of_int conf.turnstile_radius); subtree_sep_adjustment#set_value (float_of_int conf.subtree_sep); @@ -734,35 +698,25 @@ debug_check_box#set_active conf.debug_mode; tee_file_box_check_box#set_active conf.copy_input; tee_file_name_entry#set_text conf.copy_input_file; + (* print_endline "set config end"; *) () (** Change spinners and buttons to show the compile-time default configuration. *) method reset_to_default () = - self#set_configuration default_configuration + self#change_config_and_config_window default_configuration (** Switch the help/documentation tool-tips on or off, according to - the state of the help-tool-tips check box. + the argument [flag]. *) - method toggle_tooltips () = - let flag = doc_tooltip_check_box#active in - List.iter (fun misc -> misc#set_has_tooltip flag) tooltip_misc_objects; - () - - (** Change the visibility of the tee-file elements, according to the - state of the log-input check box. - *) - method tee_file_toggle () = - let flag = tee_file_box_check_box#active in - tee_file_name_label#misc#set_sensitive flag; - tee_file_name_entry#misc#set_sensitive flag; - tee_file_name_button#misc#set_sensitive flag; - () + method toggle_tooltips flag = + List.iter (fun misc -> misc#set_has_tooltip flag) tooltip_misc_objects (** Start and manage the modal file selection dialog for the log-file button. If the user makes a selection, the log-file - text entry is updated. + text entry is updated. The current configuration is then changed + via the [notify_text] signal of this entry. *) method tee_file_button_click () = let file_chooser = GWindow.file_chooser_dialog @@ -773,20 +727,23 @@ ~focus_on_map:true ~modal:true () in - file_chooser#add_select_button "Select" `SELECT; - file_chooser#add_button "Cancel" `CANCEL; + file_chooser#add_select_button_stock `APPLY `SELECT; + file_chooser#add_button_stock `CANCEL `CANCEL; ignore(file_chooser#set_current_folder (Filename.dirname tee_file_name_entry#text)); - (match file_chooser#run() with - | `SELECT -> - (match file_chooser#filename with - | None -> () - | Some file -> tee_file_name_entry#set_text file - ) - | `CANCEL - | `DELETE_EVENT -> () - ); + let chooser_file = + match file_chooser#run() with + | `SELECT -> file_chooser#filename + | `CANCEL + | `DELETE_EVENT -> None + in file_chooser#destroy(); + (match chooser_file with + | Some file -> + clean_tee_file_check_box <- false; + tee_file_name_entry#set_text file + | None -> () + ); () (** Create a new configuration record with the current values of the @@ -862,11 +819,61 @@ in update_sizes c - (** Action for the Apply button: Extract a configuration record and - update the current configuration. + (** Callback when any item of the configuration changed. This simply + updates the complete configuration in the whole program. *) - method apply () = - update_configuration (self#extract_configuration) + method config_changed () = + (* Printf.printf "change config delay %b\n%!" delay_config_update; *) + if not delay_config_update then begin + (* let app_start = U.gettimeofday () in *) + let c = self#extract_configuration in + self#toggle_tooltips c.display_doc_tooltips; + (try + update_configuration c; + with + | Log_input_file_error msg -> + run_message_dialog + (Printf.sprintf + "Opening the input log file failed with\n %s.\n\ + Disabeling input logging." + msg) + `WARNING; + tee_file_box_check_box#set_active false + ); + (* + * let app_end = U.gettimeofday () in + * Printf.printf "apply config %f ms\n%!" ((app_end -. app_start) *. 1000.) + *) + end + + (** Update the current configuration record and all displayed values + in the config window. This method makes sure that the body of + the callback {config_changed} is only executed ones and that the + input logging flag is not reset. + *) + method private change_config_and_config_window c = + delay_config_update <- true; + clean_tee_file_check_box <- false; + self#set_configuration c; + delay_config_update <- false; + self#config_changed () + + (** Callback for the case that the log file entry has changed. To + avoid lots of file openings, the tee file check box is disabled. + *) + method log_file_entry_changed (_ : string) = + (* Printf.printf "log entry start clean %b\n%!" clean_tee_file_check_box; *) + if clean_tee_file_check_box then begin + let delay = delay_config_update in + delay_config_update <- true; + tee_file_box_check_box#set_active false; + delay_config_update <- delay; + end; + clean_tee_file_check_box <- true; + (* print_endline "log entry middle"; *) + self#config_changed (); + (* print_endline "log entry end"; *) + () (** Action for the Save button: Saves the current configuration in the user specific configuration file {!config_file_location}. If @@ -874,59 +881,37 @@ configuration, a suitable warning is displayed. *) method save () = - let do_save = ref true in - if self#extract_configuration <> !current_config - then begin - let proceed_dialog = GWindow.message_dialog - ~message:"The save operation writes the current configuration \ - record to disk. However, the current configuration \ - record differs from what the configuration dialog now \ - shows (because there are changes that have not been \ - applied). Proceed anyway?" - ~message_type:`QUESTION - ~buttons:GWindow.Buttons.yes_no () - in - (match proceed_dialog#run () with - | `YES -> () - | `NO - | `DELETE_EVENT -> do_save := false - ); - proceed_dialog#destroy () - end; - if !do_save - then - try - write_config_file config_file_location !current_config - with - | Sys_error s when Util.string_ends s "Permission denied" -> - run_message_dialog - ("No permission to write the configuration file at " - ^ config_file_location ^ "!") - `WARNING - | e -> - let backtrace = Printexc.get_backtrace () in - let buf = Buffer.create 4095 in - let print_backtrace = ref !current_config.debug_mode in - (match e with - | e -> - Buffer.add_string buf "Internal error: Escaping exception "; - Buffer.add_string buf (Printexc.to_string e); - Buffer.add_string buf " in write_config_file"; - (match e with - | U.Unix_error(error, _func, _info) -> - Buffer.add_char buf '\n'; - Buffer.add_string buf (U.error_message error); - | _ -> () - ) - ); - if !print_backtrace then begin - Buffer.add_char buf '\n'; - Buffer.add_string buf backtrace; - end; - prerr_endline (Buffer.contents buf); - run_message_dialog (Buffer.contents buf) `WARNING; - () - + try + write_config_file config_file_location !current_config + with + | Sys_error s when Util.string_ends s "Permission denied" -> + run_message_dialog + ("No permission to write the configuration file at " + ^ config_file_location ^ "!") + `WARNING + | e -> + let backtrace = Printexc.get_backtrace () in + let buf = Buffer.create 4095 in + let print_backtrace = ref !current_config.debug_mode in + (match e with + | e -> + Buffer.add_string buf "Internal error: Escaping exception "; + Buffer.add_string buf (Printexc.to_string e); + Buffer.add_string buf " in write_config_file"; + (match e with + | U.Unix_error(error, _func, _info) -> + Buffer.add_char buf '\n'; + Buffer.add_string buf (U.error_message error); + | _ -> () + ) + ); + if !print_backtrace then begin + Buffer.add_char buf '\n'; + Buffer.add_string buf backtrace; + end; + prerr_endline (Buffer.contents buf); + run_message_dialog (Buffer.contents buf) `WARNING; + () (** Action for the Restore button: Restore the configuration in the the user specific configuration file {!config_file_location} as @@ -935,8 +920,7 @@ method restore () = try let c = read_config_file config_file_location in - self#set_configuration c; - update_configuration c + self#change_config_and_config_window c with | Sys_error s when Util.string_ends s "No such file or directory" -> run_message_dialog @@ -980,11 +964,16 @@ (** Action for the Cancel button and the destroy signal. *) method destroy () = config_window := None; - top_window#destroy() + top_window#destroy(); + if !start_config_dialog then exit 0 + (** Action for the Cancel button: Reset config to start time. *) + method cancel () = + self#change_config_and_config_window old_config; + self#destroy () + (** Action of the OK button. *) method ok () = - self#apply (); self#destroy () end @@ -1002,6 +991,7 @@ initializes the management object and registers all callbacks. *) let make_config_window () = + let current_config = !current_config in let top_window = GWindow.window () in let top_v_box = GPack.vbox ~packing:top_window#add () in let _config_title = GMisc.label @@ -1042,9 +1032,10 @@ let line_width_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:1 ~top:0) () in - adjustment_set_pos_int line_width_spinner#adjustment; - line_width_spinner#adjustment#set_value - (float_of_int !current_config.turnstile_line_width); + let line_width_adjustment = line_width_spinner#adjustment in + adjustment_set_pos_int line_width_adjustment; + line_width_adjustment#set_value + (float_of_int current_config.turnstile_line_width); line_width_label#misc#set_tooltip_text line_width_tooltip; line_width_spinner#misc#set_tooltip_text line_width_tooltip; @@ -1058,9 +1049,10 @@ let turnstile_size_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:1 ~top:1) () in - adjustment_set_pos_int turnstile_size_spinner#adjustment; - turnstile_size_spinner#adjustment#set_value - (float_of_int !current_config.turnstile_radius); + let turnstile_size_adjustment = turnstile_size_spinner#adjustment in + adjustment_set_pos_int turnstile_size_adjustment; + turnstile_size_adjustment#set_value + (float_of_int current_config.turnstile_radius); turnstile_size_label#misc#set_tooltip_text turnstile_size_tooltip; turnstile_size_spinner#misc#set_tooltip_text turnstile_size_tooltip; @@ -1073,9 +1065,10 @@ let line_sep_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:1 ~top:2) () in - adjustment_set_pos_int ~lower:0.0 line_sep_spinner#adjustment; - line_sep_spinner#adjustment#set_value - (float_of_int !current_config.line_sep); + let line_sep_adjustment = line_sep_spinner#adjustment in + adjustment_set_pos_int ~lower:0.0 line_sep_adjustment; + line_sep_adjustment#set_value + (float_of_int current_config.line_sep); line_sep_label#misc#set_tooltip_text line_sep_tooltip; line_sep_spinner#misc#set_tooltip_text line_sep_tooltip; @@ -1088,9 +1081,10 @@ let proof_tree_sep_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:1 ~top:3) () in - adjustment_set_pos_int ~lower:0.0 proof_tree_sep_spinner#adjustment; - proof_tree_sep_spinner#adjustment#set_value - (float_of_int !current_config.proof_tree_sep); + let proof_tree_sep_adjustment = proof_tree_sep_spinner#adjustment in + adjustment_set_pos_int ~lower:0.0 proof_tree_sep_adjustment; + proof_tree_sep_adjustment#set_value + (float_of_int current_config.proof_tree_sep); proof_tree_sep_label#misc#set_tooltip_text proof_tree_sep_tooltip; proof_tree_sep_spinner#misc#set_tooltip_text proof_tree_sep_tooltip; @@ -1103,9 +1097,10 @@ let subtree_sep_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:4 ~top:0) () in - adjustment_set_pos_int ~lower:0.0 subtree_sep_spinner#adjustment; - subtree_sep_spinner#adjustment#set_value - (float_of_int !current_config.subtree_sep); + let subtree_sep_adjustment = subtree_sep_spinner#adjustment in + adjustment_set_pos_int ~lower:0.0 subtree_sep_adjustment; + subtree_sep_adjustment#set_value + (float_of_int current_config.subtree_sep); subtree_sep_label#misc#set_tooltip_text subtree_sep_tooltip; subtree_sep_spinner#misc#set_tooltip_text subtree_sep_tooltip; @@ -1118,9 +1113,10 @@ let command_length_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:4 ~top:1) () in - adjustment_set_pos_int command_length_spinner#adjustment; - command_length_spinner#adjustment#set_value - (float_of_int !current_config.proof_command_length); + let command_length_adjustment = command_length_spinner#adjustment in + adjustment_set_pos_int command_length_adjustment; + command_length_adjustment#set_value + (float_of_int current_config.proof_command_length); command_length_label#misc#set_tooltip_text command_length_tooltip; command_length_spinner#misc#set_tooltip_text command_length_tooltip; @@ -1132,9 +1128,10 @@ let level_dist_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:4 ~top:2) () in - adjustment_set_pos_int level_dist_spinner#adjustment; - level_dist_spinner#adjustment#set_value - (float_of_int !current_config.level_distance); + let level_dist_adjustment = level_dist_spinner#adjustment in + adjustment_set_pos_int level_dist_adjustment; + level_dist_adjustment#set_value + (float_of_int current_config.level_distance); level_dist_label#misc#set_tooltip_text level_dist_tooltip; level_dist_spinner#misc#set_tooltip_text level_dist_tooltip; @@ -1147,9 +1144,10 @@ let layer_sep_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(tree_frame_table#attach ~left:4 ~top:3) () in - adjustment_set_pos_int layer_sep_spinner#adjustment; - layer_sep_spinner#adjustment#set_value - (float_of_int !current_config.layer_sep); + let layer_sep_adjustment = layer_sep_spinner#adjustment in + adjustment_set_pos_int layer_sep_adjustment; + layer_sep_adjustment#set_value + (float_of_int current_config.layer_sep); layer_sep_label#misc#set_tooltip_text layer_sep_tooltip; layer_sep_spinner#misc#set_tooltip_text layer_sep_tooltip; @@ -1172,7 +1170,7 @@ ~packing:(font_frame_table#attach ~left:0 ~top:0) () in let tree_font_button = GButton.font_button ~title:"Proof Tree Font" - ~font_name:!current_config.proof_tree_font + ~font_name:current_config.proof_tree_font ~packing:(font_frame_table#attach ~left:1 ~top:0) () in tree_font_button#set_use_size true; tree_font_button#set_use_font true; @@ -1186,7 +1184,7 @@ ~packing:(font_frame_table#attach ~left:0 ~top:1) () in let sequent_font_button = GButton.font_button ~title:"Sequent Window Font" - ~font_name:!current_config.sequent_font + ~font_name:current_config.sequent_font ~packing:(font_frame_table#attach ~left:1 ~top:1) () in sequent_font_button#set_use_size true; sequent_font_button#set_use_font true; @@ -1324,7 +1322,7 @@ ~packing:(misc_frame_table#attach ~left:0 ~right:2 ~top:misc_line) () in let doc_tooltip_check_box = GButton.check_button ~label:"Display help tool tips" - ~active:!current_config.display_doc_tooltips + ~active:current_config.display_doc_tooltips ~packing:doc_tooltip_alignment#add () in doc_tooltip_alignment#misc#set_tooltip_text doc_tooltip_tooltip; @@ -1337,7 +1335,7 @@ ~packing:(misc_frame_table#attach ~left:0 ~right:2 ~top:misc_line) () in let turnstile_tooltip_check_box = GButton.check_button ~label:"Display turnstile tool tips" - ~active:!current_config.display_turnstile_tooltips + ~active:current_config.display_turnstile_tooltips ~packing:turnstile_tooltip_alignment#add () in turnstile_tooltip_alignment#misc#set_tooltip_text turnstile_tooltip_tooltip; @@ -1350,7 +1348,7 @@ ~packing:(misc_frame_table#attach ~left:0 ~right:2 ~top:misc_line) () in let command_tooltip_check_box = GButton.check_button ~label:"Display command tool tips" - ~active:!current_config.display_command_tooltips + ~active:current_config.display_command_tooltips ~packing:command_tooltip_alignment#add () in command_tooltip_alignment#misc#set_tooltip_text command_tooltip_tooltip; @@ -1364,11 +1362,12 @@ let drag_accel_spinner = GEdit.spin_button ~digits:2 ~numeric:true ~packing:(misc_frame_table#attach ~left:1 ~top:misc_line) () in - drag_accel_spinner#adjustment#set_bounds + let drag_accel_adjustment = drag_accel_spinner#adjustment in + drag_accel_adjustment#set_bounds ~lower:(-99.0) ~upper:99.0 ~step_incr:0.01 ~page_incr:1.0 (); - drag_accel_spinner#adjustment#set_value - !current_config.button_1_drag_acceleration; + drag_accel_adjustment#set_value + current_config.button_1_drag_acceleration; drag_accel_label#misc#set_tooltip_text drag_accel_tooltip; drag_accel_spinner#misc#set_tooltip_text drag_accel_tooltip; @@ -1381,11 +1380,12 @@ let default_size_width_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(misc_frame_table#attach ~left:1 ~top:misc_line) () in - default_size_width_spinner#adjustment#set_bounds + let default_size_width_adjustment = default_size_width_spinner#adjustment in + default_size_width_adjustment#set_bounds ~lower:(-9999.0) ~upper:9999.0 ~step_incr:1.0 ~page_incr:100.0 (); - default_size_width_spinner#adjustment#set_value - (float_of_int !current_config.default_width_proof_tree_window); + default_size_width_adjustment#set_value + (float_of_int current_config.default_width_proof_tree_window); let _x_label = GMisc.label ~text:"\195\151" (* multiplication sign U+00D7 *) ~xpad:5 @@ -1393,11 +1393,12 @@ let default_size_height_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(misc_frame_table#attach ~left:3 ~top:misc_line) () in - default_size_height_spinner#adjustment#set_bounds + let default_size_height_adjustment = default_size_height_spinner#adjustment in + default_size_height_adjustment#set_bounds ~lower:(-9999.0) ~upper:9999.0 ~step_incr:1.0 ~page_incr:100.0 (); - default_size_height_spinner#adjustment#set_value - (float_of_int !current_config.default_height_proof_tree_window); + default_size_height_adjustment#set_value + (float_of_int current_config.default_height_proof_tree_window); default_size_label#misc#set_tooltip_text default_size_tooltip; default_size_width_spinner#misc#set_tooltip_text default_size_tooltip; default_size_height_spinner#misc#set_tooltip_text default_size_tooltip; @@ -1414,9 +1415,10 @@ let internal_seq_lines_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(misc_frame_table#attach ~left:1 ~top:misc_line) () in - adjustment_set_pos_int ~lower:0.0 internal_seq_lines_spinner#adjustment; - internal_seq_lines_spinner#adjustment#set_value - (float_of_int !current_config.internal_sequent_window_lines); + let internal_seq_lines_adjustment = internal_seq_lines_spinner#adjustment in + adjustment_set_pos_int ~lower:0.0 internal_seq_lines_adjustment; + internal_seq_lines_adjustment#set_value + (float_of_int current_config.internal_sequent_window_lines); internal_seq_lines_label#misc#set_tooltip_text internal_seq_lines_tooltip; internal_seq_lines_spinner#misc#set_tooltip_text internal_seq_lines_tooltip; @@ -1430,9 +1432,10 @@ let external_node_lines_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(misc_frame_table#attach ~left:1 ~top:misc_line) () in - adjustment_set_pos_int external_node_lines_spinner#adjustment; - external_node_lines_spinner#adjustment#set_value - (float_of_int !current_config.node_window_max_lines); + let external_node_lines_adjustment = external_node_lines_spinner#adjustment in + adjustment_set_pos_int external_node_lines_adjustment; + external_node_lines_adjustment#set_value + (float_of_int current_config.node_window_max_lines); external_node_lines_label#misc#set_tooltip_text external_node_lines_tooltip; external_node_lines_spinner#misc#set_tooltip_text external_node_lines_tooltip; @@ -1446,9 +1449,10 @@ let ext_table_lines_spinner = GEdit.spin_button ~digits:0 ~numeric:true ~packing:(misc_frame_table#attach ~left:1 ~top:misc_line) () in - adjustment_set_pos_int ext_table_lines_spinner#adjustment; - ext_table_lines_spinner#adjustment#set_value - (float_of_int !current_config.ext_table_lines); + let ext_table_lines_adjustment = ext_table_lines_spinner#adjustment in + adjustment_set_pos_int ext_table_lines_adjustment; + ext_table_lines_adjustment#set_value + (float_of_int current_config.ext_table_lines); ext_table_lines_label#misc#set_tooltip_text ext_table_lines_tooltip; ext_table_lines_spinner#misc#set_tooltip_text ext_table_lines_tooltip; @@ -1490,7 +1494,7 @@ ~packing:(debug_frame_table#attach ~left:0 ~right:4 ~top:0) () in let debug_check_box = GButton.check_button ~label:"More debug information" - ~active:!current_config.debug_mode + ~active:current_config.debug_mode ~packing:debug_alignment#add () in debug_alignment#misc#set_tooltip_text debug_tooltip; @@ -1501,24 +1505,29 @@ ~packing:(debug_frame_table#attach ~left:0 ~right:4 ~top:1) () in let tee_file_box_check_box = GButton.check_button ~label:"Log Proof General input" - ~active:!current_config.copy_input + ~active:current_config.copy_input ~packing:tee_file_box_alignment#add () in tee_file_box_alignment#misc#set_tooltip_text tee_file_box_tooltip; (* tee file filename *) - let tee_file_name_label = GMisc.label + let _tee_file_name_label = GMisc.label ~text:"Log file" ~xalign:0.0 ~xpad:5 ~packing:(debug_frame_table#attach ~left:0 ~top:2) () in let tee_file_name_entry = GEdit.entry - ~text:!current_config.copy_input_file + ~text:current_config.copy_input_file (* ~max_length:25 *) ~packing:(debug_frame_table#attach ~left:1 ~top:2) () in let _button_separator = GMisc.label ~text:"" ~xpad:5 ~packing:(debug_frame_table#attach ~left:2 ~top:2) () in let tee_file_name_button = GButton.button - ~label:"Log-file selection dialog" + ~label:"Change log file" ~packing:(debug_frame_table#attach ~left:3 ~top:2) () in - + (* XXX try again when lablgtk has the file-set signal for + * file chooser_button's. Tried last with lablgtk 2.16 for GTK 2.12. + * + * let file_chooser_button = GFile.chooser_button ~action:`SAVE + * ~title:"title" ~packing:(debug_frame_table#attach ~left:3 ~top:3) () in + *) (**************************************************************************** * @@ -1531,28 +1540,28 @@ *) let button_box = GPack.hbox ~spacing:5 (* ~border_width:5 *) ~packing:top_v_box#pack () in - let reset_button = GButton.button + let reset_button = GButton.button (* XXX find stock item *) ~label:"Set defaults" ~packing:button_box#pack () in - let apply_button = GButton.button - ~label:"Apply" ~packing:button_box#pack () in let cancel_button = GButton.button - ~label:"Cancel" ~packing:button_box#pack () in + ~stock:`CANCEL ~packing:button_box#pack () in let ok_button = GButton.button - ~label:"OK" ~packing:button_box#pack () in + ~stock:`OK ~packing:button_box#pack () in let restore_button = GButton.button - ~label:"Restore" ~packing:(button_box#pack ~from:`END) () in + ~stock:`REVERT_TO_SAVED ~packing:(button_box#pack ~from:`END) () in let save_button = GButton.button - ~label:"Save" ~packing:(button_box#pack ~from:`END) () in + ~stock:`SAVE ~packing:(button_box#pack ~from:`END) () in let config_window = - new config_window top_window - line_width_spinner - turnstile_size_spinner - line_sep_spinner - proof_tree_sep_spinner - subtree_sep_spinner - command_length_spinner - level_dist_spinner - layer_sep_spinner + new config_window + current_config + top_window + line_width_adjustment + turnstile_size_adjustment + line_sep_adjustment + proof_tree_sep_adjustment + subtree_sep_adjustment + command_length_adjustment + level_dist_adjustment + layer_sep_adjustment tree_font_button sequent_font_button current_color_button @@ -1563,17 +1572,17 @@ (* mark_subtree_color_button *) ext_create_color_button ext_inst_color_button - drag_accel_spinner + drag_accel_adjustment doc_tooltip_check_box turnstile_tooltip_check_box command_tooltip_check_box - default_size_width_spinner default_size_height_spinner - internal_seq_lines_spinner - external_node_lines_spinner - ext_table_lines_spinner + default_size_width_adjustment default_size_height_adjustment + internal_seq_lines_adjustment + external_node_lines_adjustment + ext_table_lines_adjustment debug_check_box tee_file_box_check_box - tee_file_name_label tee_file_name_entry tee_file_name_button + tee_file_name_entry [ line_width_label#misc; line_width_spinner#misc; turnstile_size_label#misc; turnstile_size_spinner#misc; line_sep_label#misc; line_sep_spinner#misc; @@ -1608,18 +1617,37 @@ in top_window#set_title "Prooftree Configuration"; - config_window#toggle_tooltips (); - config_window#tee_file_toggle(); - ignore(doc_tooltip_check_box#connect#toggled - ~callback:config_window#toggle_tooltips); - ignore(tee_file_box_check_box#connect#toggled - ~callback:config_window#tee_file_toggle); + config_window#toggle_tooltips current_config.display_doc_tooltips; + List.iter (fun adj -> ignore(adj#connect#value_changed + ~callback:config_window#config_changed)) + [line_width_adjustment; turnstile_size_adjustment; line_sep_adjustment; + proof_tree_sep_adjustment; subtree_sep_adjustment; + command_length_adjustment; level_dist_adjustment; layer_sep_adjustment; + drag_accel_adjustment; default_size_width_adjustment; + default_size_height_adjustment; internal_seq_lines_adjustment; + external_node_lines_adjustment; ext_table_lines_adjustment; + ]; + List.iter (fun fb -> ignore (fb#connect#font_set + ~callback:config_window#config_changed)) + [tree_font_button; sequent_font_button]; + List.iter (fun cb -> ignore (cb#connect#color_set + ~callback:config_window#config_changed)) + [current_color_button; cheated_color_button; proved_complete_color_button; + proved_incomplete_color_button; proved_partial_color_button; + ext_create_color_button; ext_inst_color_button + ]; + List.iter (fun cb -> ignore (cb#connect#toggled + ~callback:config_window#config_changed)) + [doc_tooltip_check_box; turnstile_tooltip_check_box; + command_tooltip_check_box; debug_check_box; tee_file_box_check_box + ]; + ignore(tee_file_name_entry#connect#notify_text + ~callback:config_window#log_file_entry_changed); ignore(tee_file_name_button#connect#clicked ~callback:config_window#tee_file_button_click); ignore(top_window#connect#destroy ~callback:config_window#destroy); ignore(reset_button#connect#clicked ~callback:config_window#reset_to_default); - ignore(apply_button#connect#clicked ~callback:config_window#apply); - ignore(cancel_button#connect#clicked ~callback:config_window#destroy); + ignore(cancel_button#connect#clicked ~callback:config_window#cancel); ignore(ok_button#connect#clicked ~callback:config_window#ok); ignore(save_button#connect#clicked ~callback:config_window#save); ignore(restore_button#connect#clicked ~callback:config_window#restore); diff -Nru prooftree-0.12/configure prooftree-0.13/configure --- prooftree-0.12/configure 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/configure 2017-01-03 10:35:43.000000000 +0000 @@ -4,7 +4,7 @@ # # Configuration script for prooftree # -# Hendrik Tews Copyright (C) 2011 - 2013 +# Hendrik Tews Copyright (C) 2011 - 2016 # # This file is part of "prooftree". # @@ -22,7 +22,7 @@ # You should have received a copy of the GNU General Public License # along with "prooftree". If not, see . # -# $Id: configure,v 1.6 2013/03/28 08:02:00 tews Exp $ +# $Id: configure,v 1.7 2016/01/23 12:57:13 tews Exp $ # ############################################################################## diff -Nru prooftree-0.12/coq.ml prooftree-0.13/coq.ml --- prooftree-0.12/coq.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/coq.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: coq.ml,v 1.3 2013/03/28 08:02:00 tews Exp $ + * $Id: coq.ml,v 1.5 2016/01/23 12:57:13 tews Exp $ *) @@ -42,7 +42,7 @@ (** This function parses one evar uid without the question mark. *) let coq_parse_evar_without_question scan_buf = - Scanf.bscanf scan_buf " %[0-9] " (fun evar -> evar) + Scanf.bscanf scan_buf " %[A-Za-z0-9] " (fun evar -> evar) (** This function parses the dependency list that follows ``using'', diff -Nru prooftree-0.12/.cvsignore prooftree-0.13/.cvsignore --- prooftree-0.12/.cvsignore 2012-03-06 14:57:44.000000000 +0000 +++ prooftree-0.13/.cvsignore 1970-01-01 00:00:00.000000000 +0000 @@ -1,10 +0,0 @@ -*.cmi -*.cmo -*.cmx -Makefile -Makefile.deps -dump.odoc-dump -prooftree -prooftree.man.html -prooftree.man.txt -version.ml diff -Nru prooftree-0.12/debian/changelog prooftree-0.13/debian/changelog --- prooftree-0.12/debian/changelog 2016-12-21 21:26:14.000000000 +0000 +++ prooftree-0.13/debian/changelog 2017-01-03 15:29:09.000000000 +0000 @@ -1,20 +1,11 @@ -prooftree (0.12-2build3) zesty; urgency=medium +prooftree (0.13-1) unstable; urgency=medium - * Rebuild against new OCAML ABI. + * Imported Upstream version 0.13 + * delete patch 0001-Fix-compilation-with-OCaml-4.02 (problem fixed upstream) + * push standards version to 3.9.8 + * fix some lintian warnings - -- Gianfranco Costamagna Wed, 21 Dec 2016 22:26:14 +0100 - -prooftree (0.12-2build2) zesty; urgency=medium - - * Rebuild against new OCaml ABI. - - -- Gianfranco Costamagna Wed, 21 Dec 2016 15:14:31 +0100 - -prooftree (0.12-2build1) xenial; urgency=medium - - * No-change rebuild against ocaml 4.02. - - -- Łukasz 'sil2100' Zemczak Wed, 04 Nov 2015 17:18:33 -0600 + -- Hendrik Tews Tue, 03 Jan 2017 16:29:09 +0100 prooftree (0.12-2) unstable; urgency=low diff -Nru prooftree-0.12/debian/control prooftree-0.13/debian/control --- prooftree-0.12/debian/control 2015-10-14 08:11:01.000000000 +0000 +++ prooftree-0.13/debian/control 2017-01-03 15:29:09.000000000 +0000 @@ -9,10 +9,10 @@ dh-ocaml (>= 0.9~), ocaml-best-compilers, liblablgtk2-ocaml-dev -Standards-Version: 3.9.4 +Standards-Version: 3.9.8 Homepage: http://askra.de/software/prooftree -Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/prooftree.git -Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/prooftree.git +Vcs-Git: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/prooftree.git +Vcs-Browser: https://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/prooftree.git Package: prooftree Architecture: any diff -Nru prooftree-0.12/debian/patches/0001-Fix-compilation-with-OCaml-4.02.patch prooftree-0.13/debian/patches/0001-Fix-compilation-with-OCaml-4.02.patch --- prooftree-0.12/debian/patches/0001-Fix-compilation-with-OCaml-4.02.patch 2015-10-14 08:11:01.000000000 +0000 +++ prooftree-0.13/debian/patches/0001-Fix-compilation-with-OCaml-4.02.patch 1970-01-01 00:00:00.000000000 +0000 @@ -1,60 +0,0 @@ -From: Stephane Glondu -Date: Tue, 16 Jun 2015 09:30:01 +0200 -Subject: Fix compilation with OCaml 4.02 - ---- - input.ml | 12 ++++++------ - 1 file changed, 6 insertions(+), 6 deletions(-) - -diff --git a/input.ml b/input.ml -index 934943c..8188fce 100644 ---- a/input.ml -+++ b/input.ml -@@ -55,7 +55,7 @@ - - In the following list - of commands, ``%d'' stands for a positive integer and %s for a string -- which contains no white space. ``\{cheated|not-cheated\}'' denotes -+ which contains no white space. ... denotes - the alternative of either ``cheated'' or ``not-cheated''. An - integer following the keyword state is a state number. An integer - following some xxx-bytes denotes the number of bytes of the next -@@ -79,7 +79,7 @@ - the first message. - } - {- {v current-goals state %d current-sequent %s \ -- {cheated|not-cheated} {new-layer|current-layer} proof-name-bytes %d \ -+ ... ... proof-name-bytes %d \ - command-bytes %d sequent-text-bytes %d additional-id-bytes %d \ - existential-bytes %d\n\ - \n\ -@@ -162,7 +162,7 @@ - {- Full name of the proof} - } - } -- {- {v branch-finished state %d {cheated|not-cheated} \ -+ {- {v branch-finished state %d ... \ - proof-name-bytes %d command-bytes %d existential-bytes %d\n\ - \n\ - \n\ -@@ -440,8 +440,8 @@ let parse_configure com_buf = - - (****************************************************************************** - ****************************************************************************** -- * current-goals state %d current-sequent %s {cheated|not-cheated} \ -- * {new-layer|current-layer} -+ * current-goals state %d current-sequent %s ... \ -+ * ... - * proof-name-bytes %d command-bytes %d sequent-text-bytes %d \ - * additional-id-bytes %d existential-bytes %d\n\ - * \n\ -@@ -625,7 +625,7 @@ let parse_switch_goal com_buf = - - - (****************************************************************************** -- * branch-finished state %d {cheated|not-cheated} \ -+ * branch-finished state %d ... \ - * proof-name-bytes %d command-bytes %d existential-bytes %d\n\ - * \n\ - * \n\ --- diff -Nru prooftree-0.12/debian/patches/series prooftree-0.13/debian/patches/series --- prooftree-0.12/debian/patches/series 2015-10-14 08:11:01.000000000 +0000 +++ prooftree-0.13/debian/patches/series 2017-01-03 15:29:09.000000000 +0000 @@ -1 +0,0 @@ -0001-Fix-compilation-with-OCaml-4.02.patch diff -Nru prooftree-0.12/draw_tree.ml prooftree-0.13/draw_tree.ml --- prooftree-0.12/draw_tree.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/draw_tree.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: draw_tree.ml,v 1.48 2013/03/28 08:02:00 tews Exp $ + * $Id: draw_tree.ml,v 1.54 2016/01/23 12:57:13 tews Exp $ *) @@ -408,8 +408,10 @@ *) method window_number : string - (** Set the content in the text buffer of this node window *) - method update_content : string -> unit + (** Update the content in the text buffer of this node window. The + argument is the updated {!proof_tree_element.sequent_text_history}. + *) + method update_content : string list -> unit (** Reconfigure and redraw the node window. Needs to be called when the configuration has been changed. Actually only the font of @@ -421,7 +423,7 @@ when the corresponding element in the proof-tree display is deleted. *) - method delete_non_sticky_node_window : unit + method delete_attached_node_window : unit end @@ -475,6 +477,7 @@ *) val drawable = drawable + (***************** inside proof_tree_element *) (** The width of this node alone in pixels. Set in the initializer of the heirs. *) val mutable width = 0 @@ -504,6 +507,7 @@ *) val mutable x_offset = 0 + (***************** inside proof_tree_element *) (** The height of this nodes subtree, counted in tree levels. At least 1, because this element occupies already some level. *) @@ -529,12 +533,32 @@ val mutable tree_layer = (None : proof_tree_element abstract_tree_container option) + (** This field is really used only inside {!turnstile}. In a + turnstile element, it holds the list of all previous versions of + the sequent text without existential information, except for the + head, with contains the current sequent {b with} existential + info. For uniform treatment of external node windows, the + reference is also used for proof commands. There, it holds just + one element, the proof command with existentials info. + + The existential info is omitted from old versions of the sequent + text, because this info is incorrect for sequents that get + updated. The problem is that the exisitentials change already + with {!Proof_tree.add_new_goal}, which happens long before + {!Proof_tree.update_sequent}. A fix for this would require a + protocol change, which is a bit too much for this little + feature. + *) + val mutable sequent_text_history = [] + + (***************************************************************************) (***************************************************************************) (** {2 Accessors / Setters} *) (***************************************************************************) (***************************************************************************) + (***************** inside proof_tree_element *) (** Accessor method of {!attribute: width}. *) method width = width @@ -563,6 +587,7 @@ method selected b = selected <- b + (***************** inside proof_tree_element *) (** Accessor method of {!attribute: existential_variables}. *) method existential_variables = existential_variables @@ -595,12 +620,25 @@ assert(tree_layer = None); tree_layer <- Some tl + (** Make {!sequent_text_history} accessible for cloning and for + reattaching external node windows. + *) + method sequent_text_history = sequent_text_history + + (** This method is only used inside {!turnstile} but declared here to + avoid downcasting during cloning. Set the sequent text history, + used when cloning. *) + method set_sequent_text_history history = + sequent_text_history <- history + + (***************************************************************************) (***************************************************************************) (** {2 Children Iterators} *) (***************************************************************************) (***************************************************************************) + (***************** inside proof_tree_element *) (** General iterator for all children. [iter_children left y a f] successively computes the [left] and [y] value of each child and calls [f left y c a] for each child [c] (starting with the @@ -639,6 +677,7 @@ (***************************************************************************) (***************************************************************************) + (***************** inside proof_tree_element *) (** Compute the height of the subtree of this element in pixels. *) method subtree_height = (subtree_levels - 1) * !current_config.level_distance + @@ -672,6 +711,7 @@ (0, 0, None) children in + (***************** inside proof_tree_element *) subtree_levels <- max_levels + 1; subtree_width <- children_width; x_offset <- @@ -711,6 +751,7 @@ (* this node's left side is right of the left margin of the first child *) first_child_offset <- 0; end; + (***************** inside proof_tree_element *) (* The real condition for the next if is * subtree_width - x_offset < width / 2 * but it has rounding issues when width is odd. @@ -741,6 +782,7 @@ * subtree_levels; *) + (***************** inside proof_tree_element *) (** Do {!update_subtree_size} in this element and all parent elements up to the root of the tree. *) @@ -773,6 +815,7 @@ (***************************************************************************) (***************************************************************************) + (***************** inside proof_tree_element *) (** Computes the left offset of [child] relative to the bounding box of its parent, which must be this node. *) method child_offset child = @@ -803,6 +846,7 @@ in (left_off, y_off) + (***************** inside proof_tree_element *) (** Computes the bounding box (that is a 4-tuple [(x_low, x_high, y_low, y_high)]) relative to the upper-left corner of the complete display. @@ -836,6 +880,7 @@ float_of_int (y_u + top)) + (***************** inside proof_tree_element *) (** Computes the x-coordinate of this node. Argument [left] must be the x-coordinate of the left side of the bounding box of this node's subtree. @@ -866,6 +911,7 @@ method virtual line_offset : float -> (int * int) + (***************** inside proof_tree_element *) (** Draw the lines from this node to all its children. @param left x-coordinate of the left side of the bounding box of @@ -889,6 +935,7 @@ restore_gc drawable gc_opt) + (***************** inside proof_tree_element *) (** Draw this element's subtree given the left side of the bounding box and the y-coordinate of this node. This is the internal draw method that iterates through the tree. @@ -917,6 +964,7 @@ (fun left y child -> child#draw_subtree left y) + (***************** inside proof_tree_element *) (** Draw this node's subtree given the left and top side of the bounding box. This is the external draw method that is called from the outside for the root of the tree. @@ -936,6 +984,7 @@ (***************************************************************************) (***************************************************************************) + (***************** inside proof_tree_element *) (** Iterate over the proof tree to determine the node that contains the point [(bx, by)]. Returns [None] if there is no node that contains this point. (If [bx] and [by] are the coordinates of a @@ -967,6 +1016,7 @@ None + (***************** inside proof_tree_element *) (** Iterate over the proof tree to determine the node that contains the point [(bx, by)]. Returns [None] if there is no node that contains this point. This is the external version that is called @@ -998,6 +1048,7 @@ | Some p -> p#mark_branch f | None -> () + (***************** inside proof_tree_element *) (** Mark this element as [CurrentNode] and all the parent nodes as [Current] branch, see {!branch_state_type}. Relies on the invariant that the parent of a [Current] element is also marked @@ -1029,6 +1080,7 @@ else false ) + (***************** inside proof_tree_element *) (** Mark this node as [Cheated] and mark all parents that have only [Cheated] children as [Cheated] as well, see {!branch_state_type}. @@ -1057,6 +1109,7 @@ | Cheated -> assert false ) + (***************** inside proof_tree_element *) (** Remove the [Proved] or [Cheated] mark of this element and all parent elements until an [Unproven] or [Current] element is met, see {!branch_state_type}. @@ -1094,7 +1147,8 @@ (***************************************************************************) (***************************************************************************) - (** Return the displayed sequent text for turnstile elements, which + (***************** inside proof_tree_element *) + (** Return the displayed text for proof-tree elements, which contains additional information about uninstantiated and partially instantiated existentials. *) @@ -1128,10 +1182,11 @@ method delete_external_window win = external_windows <- List.filter (fun w -> w <> win) external_windows + (***************** inside proof_tree_element *) (** Delete all non-sticky external node windows of this node. *) method delete_non_sticky_external_windows = - List.iter (fun w -> w#delete_non_sticky_node_window) external_windows + List.iter (fun w -> w#delete_attached_node_window) external_windows (** Propagate this nodes existentials to all its children. This method is not recursive. It is used during normal operation, @@ -1150,18 +1205,24 @@ List.iter (fun c -> c#propagate_existentials) children (** Update the list of existential variables in displayed sequent - text in the whole subtree of this element. This needs to be - called when some existential got instantiated or when an undo - uninstantiates some existential. + text and proof commands in the whole subtree of this element. + This needs to be called when some existential got instantiated + or when an undo uninstantiates some existential. *) method update_existentials_info = + (match sequent_text_history with + | [] -> () + | _ :: history -> + sequent_text_history <- self#displayed_text :: history + ); (if external_windows <> [] && existential_variables <> [] then - let new_text = self#displayed_text in - List.iter (fun ew -> ew#update_content new_text) external_windows + List.iter (fun ew -> ew#update_content sequent_text_history) + external_windows ); List.iter (fun c -> c#update_existentials_info) children + (***************** inside proof_tree_element *) (** Hook to be called when the list of children has been changed. Adjusts the relative layout information of this element and all its parents and (non-recursively) propagates the existentials to all @@ -1200,12 +1261,15 @@ It's value is arbitrary for cloned proof trees. *) class turnstile (drawable : better_drawable) - undo_state sequent_id sequent_text = + undo_state sequent_id sequent_text_option = object (self) inherit proof_tree_element drawable undo_state sequent_id [] [] as super (** The pure sequent text. *) - val mutable sequent_text = (sequent_text : string) + val mutable sequent_text = + match sequent_text_option with + | Some t -> t + | None -> "waiting for sequent text" (** Pango layout for rendering text. Only created if an ID for an external window must be put into the display. @@ -1228,12 +1292,33 @@ *) method id = sequent_id - (** Update the sequent text. *) - method update_sequent new_text = + (***************** inside turnstile *) + (** Update the sequent text to a new version. *) + method update_sequent new_text = + (match sequent_text_history with + | [] -> () + | _ :: old -> sequent_text_history <- sequent_text :: old + ); sequent_text <- new_text; - let new_text = self#displayed_text in - List.iter - (fun ew -> ew#update_content new_text) + sequent_text_history <- self#displayed_text :: sequent_text_history; + List.iter (fun ew -> ew#update_content sequent_text_history) + external_windows + + (** Restore the previous version of the sequent text. *) + method undo_update_sequent = + (match sequent_text_history with + | [] -> assert false + | _ :: [] -> + (* This happens when undoing the initial update sequent + * command for additional subgoals. + *) + sequent_text_history <- []; + sequent_text <- "no sequent text available" + | _ :: old :: rest -> + sequent_text <- old; + sequent_text_history <- self#displayed_text :: rest + ); + List.iter (fun ew -> ew#update_content sequent_text_history) external_windows (** Return the pango layout object of {!layout}. Create one if there @@ -1256,6 +1341,7 @@ layout <- None; super#configuration_updated + (***************** inside turnstile *) (** Draw the turnstile symbol for this sequent at the indicated coordinates. *) @@ -1293,7 +1379,7 @@ layout ) - + (***************** inside turnstile *) (** Draw this turnstile node. @param left x-coordinate of the left side of the bounding box of @@ -1328,6 +1414,7 @@ 2 * !current_config.turnstile_radius + 2 * !current_config.turnstile_line_width + (***************** inside turnstile *) initializer self#set_node_size; (* @@ -1335,6 +1422,11 @@ * self#debug_name width height; *) self#update_subtree_size; + (match sequent_text_option with + | None -> () + | Some _ -> + sequent_text_history <- [self#displayed_text] + ); () end @@ -1400,6 +1492,7 @@ (** Height (in pixels) of the rendered proof command text. *) val mutable layout_height = 0 + (***************** inside proof_command_length *) (** This is a [Proof_command] element, see {!node_kind}. *) method node_kind = Proof_command @@ -1429,6 +1522,7 @@ layout_width <- w; layout_height <- h + (***************** inside proof_command_length *) (** Set {!displayed_command}. Called from the initializer and when the configuration has been changed. *) @@ -1463,6 +1557,7 @@ layout <- make_layout drawable_arg#pango_context; super#configuration_updated + (***************** inside proof_command_length *) (** Override {!proof_tree_element.register_external_window} because the displayed proof command must be rerendered when an external window is registered. @@ -1479,6 +1574,7 @@ super#delete_external_window win; self#render_proof_command + (***************** inside proof_command_length *) (** Draw just this command node. @param left x-coordinate of the left side of the bounding box of @@ -1513,6 +1609,7 @@ drawable#rectangle ~x:(x - w/2) ~y:(y - h/2) ~width:w ~height:h (); + (***************** inside proof_command_length *) (** Compute the line offsets for proof-command nodes, see {!proof_tree_element.line_offset} *) @@ -1540,6 +1637,7 @@ * self#debug_name w width height; *) self#update_subtree_size; + sequent_text_history <- [self#displayed_text]; (* Printf.fprintf (debugc()) "INIT PC %s done\n%!" self#debug_name; *) () @@ -1587,7 +1685,10 @@ (List.map (clone_existentials ex_hash) node#fresh_existentials) : proof_command :> proof_tree_element) | Turnstile -> - (new_seq node#id node#content : turnstile :> proof_tree_element) + let ts = new_seq node#id (Some node#content) + in + ts#set_sequent_text_history node#sequent_text_history; + (ts : turnstile :> proof_tree_element) in if Some node = old_selected then cloned_selected := Some clone; diff -Nru prooftree-0.12/emacs_commands.ml prooftree-0.13/emacs_commands.ml --- prooftree-0.12/emacs_commands.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/emacs_commands.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: emacs_commands.ml,v 1.5 2013/03/28 08:02:00 tews Exp $ + * $Id: emacs_commands.ml,v 1.6 2016/01/23 12:57:14 tews Exp $ *) diff -Nru prooftree-0.12/ext_dialog.ml prooftree-0.13/ext_dialog.ml --- prooftree-0.12/ext_dialog.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/ext_dialog.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: ext_dialog.ml,v 1.15 2013/03/28 08:02:00 tews Exp $ + * $Id: ext_dialog.ml,v 1.18 2016/01/23 12:57:14 tews Exp $ *) (** The Existential Variable Dialog *) @@ -436,11 +436,11 @@ method key_pressed_callback ev = match GdkEvent.Key.keyval ev with | ks when - (ks = GdkKeysyms._Q or ks = GdkKeysyms._q) + (ks = GdkKeysyms._Q || ks = GdkKeysyms._q) && (List.mem `CONTROL (GdkEvent.Key.state ev)) -> exit 0 - | ks when (ks = GdkKeysyms._Q or ks = GdkKeysyms._q) -> + | ks when (ks = GdkKeysyms._Q || ks = GdkKeysyms._q) -> self#destroy (); true | ks when ks = GdkKeysyms._Up -> scroll_adjustment table_v_adjustment (-1); true @@ -598,7 +598,7 @@ let show_current_button = GButton.button ~label:"Show current" ~packing:button_box#pack () in let close_button = GButton.button - ~label:"Close" ~packing:(button_box#pack ~from:`END) () in + ~stock:`CLOSE ~packing:(button_box#pack ~from:`END) () in let ext_window = new existential_variable_window proof_window top_window diff -Nru prooftree-0.12/.gitignore prooftree-0.13/.gitignore --- prooftree-0.12/.gitignore 1970-01-01 00:00:00.000000000 +0000 +++ prooftree-0.13/.gitignore 2017-01-03 10:35:43.000000000 +0000 @@ -0,0 +1,14 @@ +*~ +*.cmi +*.cmo +*.cmx +*.o +Makefile +Makefile.deps +dump.odoc-dump +prooftree +prooftree.man.html +prooftree.man.txt +version.ml +TAGS +doc diff -Nru prooftree-0.12/gtk_ext.ml prooftree-0.13/gtk_ext.ml --- prooftree-0.12/gtk_ext.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/gtk_ext.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: gtk_ext.ml,v 1.18 2013/03/28 08:02:00 tews Exp $ + * $Id: gtk_ext.ml,v 1.19 2016/01/23 12:57:14 tews Exp $ *) diff -Nru prooftree-0.12/help_window.ml prooftree-0.13/help_window.ml --- prooftree-0.12/help_window.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/help_window.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: help_window.ml,v 1.17 2013/03/28 08:02:00 tews Exp $ + * $Id: help_window.ml,v 1.24 2016/01/23 12:57:14 tews Exp $ *) @@ -64,6 +64,9 @@ let bold_proof_tree = (Bold, "Prooftree") in let bold_proof_general = (Bold, "Proof General") in + (**************************************************************************) + (***************************** Colors *************************************) + (**************************************************************************) [(Heading, "Colors"); (Default, "\n\nThe meaning of the colors in the proof tree is as follows: "); (Color !proved_complete_gdk_color, @@ -84,6 +87,9 @@ (Default, " parameters \ can be changed in the configuration dialog.\n\ \n"); + (*************************************************************************) + (***************************** Navigation ********************************) + (*************************************************************************) (Heading, "Navigation"); (Default, "\n\n\ In addition to scroll bars and the usual keys one can move the proof \ @@ -95,6 +101,9 @@ the proof tree instead (i.e, the proof tree moves in the same \ direction as the mouse).\n\ \n"); + (*************************************************************************) + (***************************** Sequent window ****************************) + (*************************************************************************) (Heading, "The sequent window and additional displays"); (Default, "\n\n\ The sequent display below the proof tree \ @@ -105,13 +114,18 @@ be set in the configuration dialog. A value of 0 hides the sequent display.\n\ \n\ A double click or a shift-click displays any goal or proof command \ -in an additional \ -window. These additional windows are deleted when the main proof-tree \ -window disappears, unless their "); - (Italic, "Sticky"); - (Default, " button is pressed.\n\ +in an additional window. These additional windows are automatically updated, \ +for instance, if an existential variable is instantiated. For additional \ +sequent displays one can browse the instantiation history of the sequent \ +using the forward and backward buttons. These additional windows can be "); + (Italic, "detached"); + (Default, " from the proof tree. A detached \ +display is neither automatically updated nor automatically deleted.\n\ \n\ "); + (*************************************************************************) + (***************************** Tooltips **********************************) + (*************************************************************************) (Heading, "Tooltips"); (Default, "\n\n\ If turnstile tool tips are switched on, the complete sequent text is \ @@ -123,6 +137,9 @@ Any truncated proof command is displayed in full length as tool tip if the \ mouse stays long enough above it (and if command tool tips are enabled).\n\ \n"); + (*************************************************************************) + (***************************** Existentials ******************************) + (*************************************************************************) (Heading, "Existential variables"); (Default, "\n\ \n"); @@ -152,7 +169,20 @@ (Background !existential_instantiate_gdk_color, "(with orange background, by default)"); (Default, " in the proof-tree display.\n\ +\n\ +With "); + (Bold, "Coq"); + (Default, " >= 8.5, existential variables are severely broken in "); + bold_proof_tree; + (Default, " because "); + (Bold, "Coq"); + (Default, " does not provide the necessary information, see "); + (Bold, "Coq"); + (Default, " bug 4504.\n\ \n"); + (*************************************************************************) + (***************************** Menus *************************************) + (*************************************************************************) (Heading, "Menus"); (Default, "\n\n\ The menu button opens the main menu. A right click opens the context menu, \ @@ -183,8 +213,10 @@ \n\ The "); (Italic, "Show current"); - (Default, " menu item repositions the proof tree such that the \ -current proof goal is visible.\n\ + (Default, " and "); + (Italic, "Show selected"); + (Default, " menu items reposition the proof tree such that the \ +current proof goal or, respectively, the selected node is visible.\n\ \n\ The item "); (Italic, "Existentials"); @@ -192,18 +224,17 @@ \n\ The "); (Italic, "Configuration"); - (Default, " item displays the configuration dialog. Changing values \ -there does only take effect after the "); - (Italic, "Apply"); - (Default, " or "); - (Italic, "OK"); - (Default, " button has been pressed. The "); + (Default, " item displays the configuration dialog. Changes in this dialog \ +immediately take effect. In this dialog, the "); (Italic, "Save"); (Default, " button stores the current configuration values \ in the file "); (Italic, config_file_location); (Default, ", which overwrites the build-in default configuration \ -at start up.\n\ +at start up. The "); + (Italic, "Cancel"); + (Default, " button closes the dialog and resets the configuration to \ +the state before starting the configuration dialog.\n\ \n\ The "); (Italic, "Exit"); @@ -215,6 +246,9 @@ bold_proof_tree; (Default, ".)\n\ \n"); + (*************************************************************************) + (***************************** Customization *****************************) + (*************************************************************************) (Heading, "Customization"); (Default, "\n\n\ A major part of the proof visualization task is done by "); @@ -259,6 +293,10 @@ help_text +(** Flag for option [-help]. *) +let start_help_dialog = ref false + + (** Create and display a new help window. This function creates a new {xref lablgtk class GWindow.dialog} that contains the formatted help text inside a {xref lablgtk class GText.view}. @@ -271,7 +309,11 @@ ~resizable:true () in - help_win#add_button "Close" `CLOSE; + let close_fun _ = + help_win#destroy (); + if !start_help_dialog then exit 0 + in + help_win#add_button_stock `CLOSE `CLOSE; let _help_title = GMisc.label ~markup:"Prooftree Help" @@ -291,8 +333,8 @@ ~packing:help_scrolling#add () in fill_help_buffer help_view#buffer; - ignore(help_win#connect#destroy ~callback:(fun () -> help_win#destroy())); - ignore(help_win#connect#response ~callback:(fun _ -> help_win#destroy())); + ignore(help_win#connect#destroy ~callback:close_fun); + ignore(help_win#connect#response ~callback:close_fun); help_win#set_default_size ~width:400 ~height:300; (* help_win#set_default_size ~width:800 ~height:800; *) help_win#show () diff -Nru prooftree-0.12/input.ml prooftree-0.13/input.ml --- prooftree-0.12/input.ml 2013-03-28 08:02:00.000000000 +0000 +++ prooftree-0.13/input.ml 2017-01-03 10:35:43.000000000 +0000 @@ -1,7 +1,7 @@ (* * prooftree --- proof tree display for Proof General * - * Copyright (C) 2011 - 2013 Hendrik Tews + * Copyright (C) 2011 - 2016 Hendrik Tews * * This file is part of "prooftree". * @@ -19,7 +19,7 @@ * You should have received a copy of the GNU General Public License * along with "prooftree". If not, see . * - * $Id: input.ml,v 1.37 2013/03/28 08:02:00 tews Exp $ + * $Id: input.ml,v 1.43 2016/01/23 12:57:14 tews Exp $ *) @@ -29,13 +29,23 @@ *****************************************************************************) (** {2 Communition Protocol with Proof General} - The communication protocol with Proof General is almost one-way - only: Proof General sends display messages to Prooftree and - Prooftree never requests anything from Proof General. Only when - the proof-tree window of the current proof is closed, Prooftree - notifies Proof General. The communication protocol is designed - such that Prooftree always knows in advance how many bytes it has - to read until the end of a display message. + The communication protocol with Proof General is mostly one-way: + Proof General sends display messages to Prooftree and Prooftree + never requests information for the proof-tree display from Proof + General. Prooftree sends a notification to Proof General when the + proof-tree window is closed. It also sends proof commands to Proof + General on request of the user. + + The communication protocol between Proof General and Prooftree is + split into two parts: The display messages, which are sent from + Proof General to Prooftree and the notification messages, which + are sent from Prooftree to Proof General. + + {3 Display Messages} + + The protocol for the display messages is designed such that + Prooftree always knows in advance how many bytes it has to read + until the end of a message. All display messages consist of {ul @@ -55,7 +65,7 @@ In the following list of commands, ``%d'' stands for a positive integer and %s for a string - which contains no white space. ``\{cheated|not-cheated\}'' denotes + which contains no white space. ``\{cheated | not-cheated\}'' denotes the alternative of either ``cheated'' or ``not-cheated''. An integer following the keyword state is a state number. An integer following some xxx-bytes denotes the number of bytes of the next @@ -79,9 +89,9 @@ the first message. } {- {v current-goals state %d current-sequent %s \ - {cheated|not-cheated} {new-layer|current-layer} proof-name-bytes %d \ - command-bytes %d sequent-text-bytes %d additional-id-bytes %d \ - existential-bytes %d\n\ + {cheated | not-cheated} {new-layer | current-layer} proof-name-bytes %d \ + command-bytes %d sequent-text-bytes %d additional-id-bytes %d \ + existential-bytes %d\n\ \n\ \n\ \n\ @@ -162,7 +172,7 @@ {- Full name of the proof} } } - {- {v branch-finished state %d {cheated|not-cheated} \ + {- {v branch-finished state %d {cheated | not-cheated} \ proof-name-bytes %d command-bytes %d existential-bytes %d\n\ \n\ \n\ @@ -207,6 +217,41 @@ } } } + + {3 Notification Messages} + + The notification messages are sent from Prooftree to Proof General + as a consequence of certain user interactions. There are 3 + different notification messages: for stopping the proof-tree + display, for undo and for sending proof scripts. All notification + messages are preceeded with a newline and the string + [emacs exec:], followed by a space, for easy recognition in Proof + General. + + The remaining part of the messages have the following format. + + {ul + {- {v stop-displaying v} + + Prooftree sends this message to Proof General when the user closed + the proof-tree display of a proof currently under development. + Proof General then stops sending display commands for that proof. + } + {- {v undo %d v} + + Prooftree sends the undo message, when the user selected an undo + for a certain sequent from the context menu. The integer is the + undo state number of the proof command child node of the selected + sequent. + } + {- {v insert-proof-script %d\n