<commit_before>(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* Why3 to HTML *)

{

  open Format
  open Lexing
  open Why3

  let output_comments = ref true

  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }

  let make_table l =
    let ht = Hashtbl.create 97 in
    List.iter (fun s -> Hashtbl.add ht s ()) l;
    Hashtbl.mem ht

  let is_keyword1 = make_table [ "as"; "axiom"; "clone"; "coinductive";
    "constant"; "else"; "end"; "epsilon"; "exists"; "export"; "false";
    "forall"; "function"; "goal"; "if"; "import"; "in"; "inductive";
    "lemma"; "let"; "match"; "meta"; "namespace"; "not"; "predicate";
    "prop"; "then"; "theory"; "true"; "type"; "use"; "with";
    (* programs *) "abstract"; "any";
    "begin"; "do"; "done"; "downto"; "exception";
    "for"; "fun"; "ghost"; "loop"; "model"; "module";
    "mutable"; "private"; "raise"; "rec";
    "to"; "try"; "val"; "while"; ]

  let is_keyword2 = make_table [ "absurd"; "assert"; "assume";
    "ensures"; "check"; "invariant"; "raises"; "reads"; "requires";
    "returns"; "variant"; "writes"; "diverges"; ]

  let get_loc lb =
    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)

  let html_char fmt c =
    pp_print_string fmt (match c with
      | '<' -> "&lt;"
      | '>' -> "&gt;"
      | '&' -> "&amp;"
      | _ -> assert false)

  let html_escape s =
    let len = ref 0 in
    String.iter (function '<' | '>' -> len := !len + 4
      | '&' -> len := !len + 5 | _ -> incr len) s;
    let len' = !len in
    let len = String.length s in
    if len = len' then s else begin
      let t = String.create len' in
      let j = ref 0 in
      let app u =
        let l = String.length u in
        String.blit u 0 t !j l;
        j := !j + l in
      for i = 0 to len - 1 do
        match s.[i] with
        | '<' -> app "&lt;"
        | '>' -> app "&gt;"
        | '&' -> app "&amp;"
        | c -> t.[!j] <- c; incr j
      done;
      t
    end

  let current_file = ref ""

  let print_ident fmt lexbuf s =
    if is_keyword1 s then
      fprintf fmt "<span class=\"keyword1\">%s</span>" s
    else if is_keyword2 s then
      fprintf fmt "<span class=\"keyword2\">%s</span>" s
    else begin
      let (* f,l,c as *) loc = get_loc lexbuf in
      (* Format.eprintf "  IDENT %s/%d/%d@." f l c; *)
      (* is this a def point? *)
      let s = html_escape s in
      try
        match Glob.find loc with
        | id, Glob.Def ->
          let t = Doc_def.anchor id in
          fprintf fmt "<a name=\"%s\">%s</a>" t s
        | id, Glob.Use ->
          let url = Doc_def.locate id in
          fprintf fmt "<a href=\"%s\">%s</a>" url s
      with Not_found ->
        (* otherwise, just print it *)
        pp_print_string fmt s
    end

  type empty_line = PrevEmpty | CurrEmpty | NotEmpty

}

let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
let prefix_op =
    op_char_1234* op_char_1 op_char_1234*
  | op_char_234*  op_char_2 op_char_234*
  | op_char_34* op_char_3 op_char_34*
  | op_char_4+
let operator =
    op_char_pref op_char_4*
  | prefix_op
  | prefix_op '_'
  | "[]"
  | "[<-]"
  | "[]<-"

let space = [' ' '\t']
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
let special = ['<' '>' '&']

rule scan fmt empty = parse
  | "(*)" as s
          { pp_print_string fmt s;
            scan fmt NotEmpty lexbuf }
  | space* "(***"
          { comment fmt false lexbuf;
            scan fmt empty lexbuf }
  | space* "(**"
          { pp_print_string fmt "</pre>\n";
            if empty <> PrevEmpty then
              pp_print_string fmt "<div class=\"info\">";
            doc fmt false [] lexbuf;
            if empty <> PrevEmpty then pp_print_string fmt "</div>";
            pp_print_string fmt "<pre>";
            scan fmt CurrEmpty lexbuf }
  | "(*"
          { pp_print_string fmt "<span class=\"comment\">(*";
            comment fmt true lexbuf;
            pp_print_string fmt "</span>";
            scan fmt NotEmpty lexbuf }
  | eof   { () }
  | ident as s
          { print_ident fmt lexbuf s;<commit_msg>why3doc: fixed bug with comment (**)<commit_after>(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* Why3 to HTML *)

{

  open Format
  open Lexing
  open Why3

  let output_comments = ref true

  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }

  let make_table l =
    let ht = Hashtbl.create 97 in
    List.iter (fun s -> Hashtbl.add ht s ()) l;
    Hashtbl.mem ht

  let is_keyword1 = make_table [ "as"; "axiom"; "clone"; "coinductive";
    "constant"; "else"; "end"; "epsilon"; "exists"; "export"; "false";
    "forall"; "function"; "goal"; "if"; "import"; "in"; "inductive";
    "lemma"; "let"; "match"; "meta"; "namespace"; "not"; "predicate";
    "prop"; "then"; "theory"; "true"; "type"; "use"; "with";
    (* programs *) "abstract"; "any";
    "begin"; "do"; "done"; "downto"; "exception";
    "for"; "fun"; "ghost"; "loop"; "model"; "module";
    "mutable"; "private"; "raise"; "rec";
    "to"; "try"; "val"; "while"; ]

  let is_keyword2 = make_table [ "absurd"; "assert"; "assume";
    "ensures"; "check"; "invariant"; "raises"; "reads"; "requires";
    "returns"; "variant"; "writes"; "diverges"; ]

  let get_loc lb =
    Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)

  let html_char fmt c =
    pp_print_string fmt (match c with
      | '<' -> "&lt;"
      | '>' -> "&gt;"
      | '&' -> "&amp;"
      | _ -> assert false)

  let html_escape s =
    let len = ref 0 in
    String.iter (function '<' | '>' -> len := !len + 4
      | '&' -> len := !len + 5 | _ -> incr len) s;
    let len' = !len in
    let len = String.length s in
    if len = len' then s else begin
      let t = String.create len' in
      let j = ref 0 in
      let app u =
        let l = String.length u in
        String.blit u 0 t !j l;
        j := !j + l in
      for i = 0 to len - 1 do
        match s.[i] with
        | '<' -> app "&lt;"
        | '>' -> app "&gt;"
        | '&' -> app "&amp;"
        | c -> t.[!j] <- c; incr j
      done;
      t
    end

  let current_file = ref ""

  let print_ident fmt lexbuf s =
    if is_keyword1 s then
      fprintf fmt "<span class=\"keyword1\">%s</span>" s
    else if is_keyword2 s then
      fprintf fmt "<span class=\"keyword2\">%s</span>" s
    else begin
      let (* f,l,c as *) loc = get_loc lexbuf in
      (* Format.eprintf "  IDENT %s/%d/%d@." f l c; *)
      (* is this a def point? *)
      let s = html_escape s in
      try
        match Glob.find loc with
        | id, Glob.Def ->
          let t = Doc_def.anchor id in
          fprintf fmt "<a name=\"%s\">%s</a>" t s
        | id, Glob.Use ->
          let url = Doc_def.locate id in
          fprintf fmt "<a href=\"%s\">%s</a>" url s
      with Not_found ->
        (* otherwise, just print it *)
        pp_print_string fmt s
    end

  type empty_line = PrevEmpty | CurrEmpty | NotEmpty

}

let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
let prefix_op =
    op_char_1234* op_char_1 op_char_1234*
  | op_char_234*  op_char_2 op_char_234*
  | op_char_34* op_char_3 op_char_34*
  | op_char_4+
let operator =
    op_char_pref op_char_4*
  | prefix_op
  | prefix_op '_'
  | "[]"
  | "[<-]"
  | "[]<-"

let space = [' ' '\t']
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
let special = ['<' '>' '&']

rule scan fmt empty = parse
  | "(*)" as s
          { pp_print_string fmt s;
            scan fmt NotEmpty lexbuf }
  | space* "(***"
          { comment fmt false lexbuf;
            scan fmt empty lexbuf }
  | space* "(**"
          { pp_print_string fmt "</pre>\n";
            if empty <> PrevEmpty then
              pp_print_string fmt "<div class=\"info\">";
            doc fmt false [] lexbuf;
            if empty <> PrevEmpty then pp_print_string fmt "</div>";
            pp_print_string fmt "<pre>";
            scan fmt CurrEmpty lexbuf }
  | "(**)"
          { pp_print_string fmt "<span class=\"comment\">(**)</span>";
            scan fmt NotEmpty lexbuf }
  | "(*"
          { pp_print_string fmt "<span class=\"comment\">(*";
            comment fmt true lexbuf;
            pp_print_string fmt "</span>";
            scan fmt NotEmpty lexbuf }
  | eof   { () }
  | ident as s
          { print_ident fmt lexbuf s;
{'fraction_non_alphanumeric': 0.18877650262594825, 'fraction_numerical': 0.015074888154055631, 'mean_word_length': 2.039609813774756, 'pattern_counts': {'":': 0, '<': 55, '<?xml version=': 0, '>': 77, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4521860', 'n_tokens_mistral': 3618, 'n_tokens_neox': 3449, 'n_words': 1002}