diff options
author | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 14:12:22 +0000 |
---|---|---|
committer | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 14:12:22 +0000 |
commit | e653960a72cbf0bd95e7cef97cd9000eb44fd267 (patch) | |
tree | 061ac7e6d97ae753a63f217adefadb0a78732ebd /ide | |
parent | 0347ba1eecdbc803e2f960074c4fd63a39c8f698 (diff) |
plus de syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5089 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coq.ml | 50 | ||||
-rw-r--r-- | ide/coq_commands.ml | 9 | ||||
-rw-r--r-- | ide/coqide.ml | 16 |
3 files changed, 54 insertions, 21 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index d8e0a04c2..54a0e4736 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -103,24 +103,42 @@ let user_error_loc l s = let interp s = prerr_endline "Starting interp..."; prerr_endline s; - let pe = Pcoq.Gram.Entry.parse - Pcoq.main_entry - (Pcoq.Gram.parsable (Stream.of_string s)) - in match pe with - | Some (loc,( VernacDefinition _ | VernacStartTheoremProof _ - | VernacBeginSection _ | VernacGoal _ - | VernacDefineModule _ | VernacDeclareModuleType _)) - when is_in_proof_mode () -> - user_error_loc loc (str "cannot do that while in proof mode.") - | Some (loc, VernacDebug _ ) -> - user_error_loc loc (str "cannot do that within CoqIDE") - | _ -> - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); - match pe with - | Some last -> + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in + match pe with + | None -> assert false + | Some((loc,vernac) as last) -> + match vernac with + | VernacDefinition _ | VernacStartTheoremProof _ + | VernacBeginSection _ | VernacGoal _ + | VernacDefineModule _ | VernacDeclareModuleType _ + when is_in_proof_mode () -> + user_error_loc loc (str "CoqIDE do not support nested goals") + | VernacDebug _ -> + user_error_loc loc (str "Debug mode not available within CoqIDE") + | VernacResetName _ + | VernacResetInitial + | VernacBack _ + | VernacAbort _ + | VernacAbortAll + | VernacRestart + | VernacSuspend + | VernacResume _ + | VernacUndo _ -> + user_error_loc loc (str "Use CoqIDE navigation instead") + | _ -> + begin + match vernac with + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ -> () + | _ -> () + end; + Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); prerr_endline ("...Done with interp of : "^s); last - | None -> assert false let interp_and_replace s = let result = interp s in diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index aefae8fbb..7173bfc2f 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -60,12 +60,11 @@ let commands = [ "Grammar";]; ["Hint"; "Hint Constructors"; - "Hint Unfold"; + "Hint Extern"; + "Hint Immediate"; + "Hint Resolve"; "Hint Rewrite"; - "Hints Extern"; - "Hints Immediate"; - "Hints Resolve"; - "Hints Unfold"; + "Hint Unfold"; "Hypothesis";]; ["Identity Coercion"; "Implicit Arguments Off."; diff --git a/ide/coqide.ml b/ide/coqide.ml index dcb3228fb..890a38bf5 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1717,6 +1717,9 @@ let create_input_tab filename = ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]); tv1 + + +let last_make = ref "";; let main files = (* Statup preferences *) @@ -2549,10 +2552,23 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); save_f (); av#insert_message "Command output:\n"; let s,res = run_command av#insert_message !current.cmd_make in + last_make := res; !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in let make_m = externals_factory#add_item "_Make" ~callback:make_f in + + (* Compile/Next Error *) + let next_error () = () +(* + let file,line,start,stop = search_next_error () in + av#insert_message + ("Error in " ^ file ^ "," ^ (string_of_int line) +*) + in + let next_error_m = externals_factory#add_item "_Next error" ~callback:next_error in + + (* Command/CoqMakefile Menu*) let coq_makefile_f () = let v = get_active_view () in |