summaryrefslogtreecommitdiff
path: root/ide/highlight.mll
diff options
context:
space:
mode:
Diffstat (limited to 'ide/highlight.mll')
-rw-r--r--ide/highlight.mll215
1 files changed, 0 insertions, 215 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll
deleted file mode 100644
index c288d6a3..00000000
--- a/ide/highlight.mll
+++ /dev/null
@@ -1,215 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: highlight.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-{
-
- open Lexing
-
- type color = GText.tag
-
- type highlight_order = int * int * color
-
- let comment_start = ref 0
-
- (* Without this table, the automaton would be too big and
- ocamllex would fail *)
- let is_one_word_command =
- let h = Hashtbl.create 97 in
- List.iter (fun s -> Hashtbl.add h s ())
- [ "Add" ; "Check"; "Eval"; "Extraction" ;
- "Load" ; "Undo"; "Goal";
- "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
- "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
- ];
- Hashtbl.mem h
-
- let is_constr_kw =
- let h = Hashtbl.create 97 in
- List.iter (fun s -> Hashtbl.add h s ())
- [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
- "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return";
- "Prop"; "Set"; "Type" ];
- Hashtbl.mem h
-
- (* Without this table, the automaton would be too big and
- ocamllex would fail *)
- let is_one_word_declaration =
- let h = Hashtbl.create 97 in
- List.iter (fun s -> Hashtbl.add h s ())
- [ (* Theorems *)
- "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ;
- "Proposition" ; "Property" ;
- (* Definitions *)
- "Definition" ; "Let" ; "Example" ; "SubClass" ;
- "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ;
- (* Assumptions *)
- "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
- "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
- (* Inductive *)
- "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
- (* Other *)
- "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class"
- ];
- Hashtbl.mem h
-
- let starting = ref true
-}
-
-let space =
- [' ' '\010' '\013' '\009' '\012']
-let firstchar =
- ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
-let identchar =
- ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
-let ident = firstchar identchar*
-
-let multiword_declaration =
- "Module" (space+ "Type")?
-| "Program" space+ ident
-| "Existing" space+ "Instance"
-| "Canonical" space+ "Structure"
-
-let locality = ("Local" space+)?
-
-let multiword_command =
- "Set" (space+ ident)*
-| "Unset" (space+ ident)*
-| "Open" space+ locality "Scope"
-| "Close" space+ locality "Scope"
-| "Bind" space+ "Scope"
-| "Arguments" space+ "Scope"
-| "Reserved" space+ "Notation" space+ locality
-| "Delimit" space+ "Scope"
-| "Next" space+ "Obligation"
-| "Solve" space+ "Obligations"
-| "Require" space+ ("Import"|"Export")?
-| "Infix" space+ locality
-| "Notation" space+ locality
-| "Hint" space+ locality ident
-| "Reset" (space+ "Initial")?
-| "Tactic" space+ "Notation"
-| "Implicit" space+ "Arguments"
-| "Implicit" space+ ("Type"|"Types")
-| "Combined" space+ "Scheme"
-| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"))|
- ("Library"|"Inline"|"NoInline"|"Blacklist"))
-| "Recursive" space+ "Extraction" (space+ "Library")?
-| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
-| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive")
-
-(* At least still missing: "Inline" + decl, variants of "Identity
- Coercion", variants of Print, Add, ... *)
-
-rule next_starting_order = parse
- | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
- | space+ { next_starting_order lexbuf }
- | multiword_declaration
- { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl }
- | multiword_command
- { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd }
- | ident as id
- { if id = "Time" then next_starting_order lexbuf else
- begin
- starting:=false;
- if is_one_word_command id then
- lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
- else if is_one_word_declaration id then
- lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl
- else
- next_interior_order lexbuf
- end
- }
- | _ { starting := false; next_interior_order lexbuf}
- | eof { raise End_of_file }
-
-and next_interior_order = parse
- | "(*"
- { comment_start := lexeme_start lexbuf; comment lexbuf }
- | ident as id
- { if is_constr_kw id then
- lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
- else
- next_interior_order lexbuf }
- | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf }
- | _ { next_interior_order lexbuf}
- | eof { raise End_of_file }
-
-and comment = parse
- | "*)" { !comment_start,lexeme_end lexbuf,Tags.Script.comment }
- | "(*" { ignore (comment lexbuf); comment lexbuf }
- | "\"" { string_in_comment lexbuf }
- | _ { comment lexbuf }
- | eof { raise End_of_file }
-
-and string_in_comment = parse
- | "\"\"" { string_in_comment lexbuf }
- | "\"" { comment lexbuf }
- | _ { string_in_comment lexbuf }
- | eof { raise End_of_file }
-
-{
- open Ideutils
-
- let highlighting = ref false
-
- let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop =
- starting := true; (* approximation: assume the beginning of a sentence *)
- if !highlighting then prerr_endline "Rejected highlight"
- else begin
- highlighting := true;
- prerr_endline "Highlighting slice now";
- input_buffer#remove_tag ~start ~stop Tags.Script.error;
- input_buffer#remove_tag ~start ~stop Tags.Script.kwd;
- input_buffer#remove_tag ~start ~stop Tags.Script.decl;
- input_buffer#remove_tag ~start ~stop Tags.Script.comment;
-
- (try begin
- let offset = start#offset in
- let s = start#get_slice ~stop in
- let convert_pos = byte_offset_to_char_offset s in
- let lb = Lexing.from_string s in
- try
- while true do
- let b,e,o =
- if !starting then next_starting_order lb
- else next_interior_order lb in
-
- let b,e = convert_pos b,convert_pos e in
- let start = input_buffer#get_iter_at_char (offset + b) in
- let stop = input_buffer#get_iter_at_char (offset + e) in
- input_buffer#apply_tag ~start ~stop o
- done
- with End_of_file -> ()
- end
- with _ -> ());
- highlighting := false
- end
-
- let highlight_current_line input_buffer =
- try
- let i = get_insert input_buffer in
- highlight_slice input_buffer (i#set_line_offset 0) i
- with _ -> ()
-
- let highlight_around_current_line input_buffer =
- try
- let i = get_insert input_buffer in
- highlight_slice input_buffer
- (i#backward_lines 10)
- (ignore (i#nocopy#forward_lines 10);i)
-
- with _ -> ()
-
- let highlight_all input_buffer =
- try
- highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
- with _ -> ()
-
-}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:09:15 +0000