diff options
Diffstat (limited to 'ide/highlight.mll')
| -rw-r--r-- | ide/highlight.mll | 92 |
1 files changed, 52 insertions, 40 deletions
diff --git a/ide/highlight.mll b/ide/highlight.mll index f2ecaa9c..3acdd4f0 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id$ *) { open Lexing - type color = string + type color = GText.tag type highlight_order = int * int * color @@ -24,7 +24,7 @@ let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) [ "Add" ; "Check"; "Eval"; "Extraction" ; - "Load" ; "Undo"; "Goal"; + "Load" ; "Undo"; "Goal"; "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]; @@ -33,9 +33,9 @@ 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"; "dest"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type" ]; + [ "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 @@ -48,7 +48,7 @@ "Proposition" ; "Property" ; (* Definitions *) "Definition" ; "Let" ; "Example" ; "SubClass" ; - "Fixpoint" ; "CoFixpoint" ; "Scheme" ; + "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ; (* Assumptions *) "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"; @@ -62,11 +62,11 @@ let starting = ref true } -let space = +let space = [' ' '\010' '\013' '\009' '\012'] -let firstchar = +let firstchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] -let identchar = +let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let ident = firstchar identchar* @@ -79,8 +79,8 @@ let multiword_declaration = let locality = ("Local" space+)? let multiword_command = - "Set" (space+ ident)* -| "Unset" (space+ ident)* + "Set" (space+ ident)* +| "Unset" (space+ ident)* | "Open" space+ locality "Scope" | "Close" space+ locality "Scope" | "Bind" space+ "Scope" @@ -98,6 +98,11 @@ let multiword_command = | "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, ... *) @@ -106,17 +111,17 @@ 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, "decl" } + { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl } | multiword_command - { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } - | ident as id + { 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, "kwd" + 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, "decl" + lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl else next_interior_order lexbuf end @@ -125,11 +130,11 @@ rule next_starting_order = parse | eof { raise End_of_file } and next_interior_order = parse - | "(*" + | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } - | ident as id + | ident as id { if is_constr_kw id then - lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd else next_interior_order lexbuf } | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf } @@ -137,42 +142,49 @@ and next_interior_order = parse | eof { raise End_of_file } and comment = parse - | "*)" { !comment_start,lexeme_end lexbuf,"comment" } + | "*)" { !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 = + 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" + if !highlighting then prerr_endline "Rejected highlight" else begin highlighting := true; prerr_endline "Highlighting slice now"; - input_buffer#remove_tag_by_name ~start ~stop "error"; - input_buffer#remove_tag_by_name ~start ~stop "kwd"; - input_buffer#remove_tag_by_name ~start ~stop "decl"; - input_buffer#remove_tag_by_name ~start ~stop "comment"; + 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 + 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_by_name ~start ~stop o + input_buffer#apply_tag ~start ~stop o done with End_of_file -> () end @@ -181,22 +193,22 @@ and comment = parse end let highlight_current_line input_buffer = - try + 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 highlight_around_current_line input_buffer = + try let i = get_insert input_buffer in - highlight_slice input_buffer - (i#backward_lines 10) + highlight_slice input_buffer + (i#backward_lines 10) (ignore (i#nocopy#forward_lines 10);i) with _ -> () - - let highlight_all input_buffer = - try + + let highlight_all input_buffer = + try highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter with _ -> () |