tuned: prefer list operations over Source.source;
authorwenzelm
Wed Jan 24 19:50:00 2018 +0100 (18 months ago)
changeset 67500dfde99d59f6e
parent 67499 bbb86f719d4b
child 67501 182a18af5b41
tuned: prefer list operations over Source.source;
approximative parsing of theory header;
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jan 24 18:54:53 2018 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jan 24 19:50:00 2018 +0100
     1.3 @@ -131,7 +131,8 @@
     1.4          | SOME id => Protocol_Message.command_positions_yxml id)
     1.5          |> error;
     1.6      val {name = (name, _), imports, ...} = header;
     1.7 -    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
     1.8 +    val {name = (_, pos), imports = imports', keywords} =
     1.9 +      Thy_Header.read_tokens Position.none span;
    1.10      val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports;
    1.11    in Thy_Header.make (name, pos) imports'' keywords end;
    1.12  
     2.1 --- a/src/Pure/Thy/thy_header.ML	Wed Jan 24 18:54:53 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Jan 24 19:50:00 2018 +0100
     2.3 @@ -23,8 +23,8 @@
     2.4    val is_base_name: string -> bool
     2.5    val import_name: string -> string
     2.6    val args: header parser
     2.7 +  val read_tokens: Position.T -> Token.T list -> header
     2.8    val read: Position.T -> string -> header
     2.9 -  val read_tokens: Token.T list -> header
    2.10  end;
    2.11  
    2.12  structure Thy_Header: THY_HEADER =
    2.13 @@ -174,27 +174,35 @@
    2.14      Parse.command_name text_rawN) --
    2.15    Parse.tags -- Parse.!!! Parse.document_source;
    2.16  
    2.17 -val header =
    2.18 +val parse_header =
    2.19    (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
    2.20  
    2.21 -fun token_source pos =
    2.22 -  Symbol.explode
    2.23 -  #> Source.of_list
    2.24 -  #> Token.source_strict bootstrap_keywords pos;
    2.25 +fun read_tokens pos toks =
    2.26 +  filter Token.is_proper toks
    2.27 +  |> Source.of_list
    2.28 +  |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! parse_header)))
    2.29 +  |> Source.get_single
    2.30 +  |> (fn SOME (header, _) => header | NONE => error ("Unexpected end of input" ^ Position.here pos));
    2.31 +
    2.32 +local
    2.33  
    2.34 -fun read_source pos source =
    2.35 -  let val res =
    2.36 -    source
    2.37 -    |> Token.source_proper
    2.38 -    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
    2.39 -    |> Source.get_single;
    2.40 -  in
    2.41 -    (case res of
    2.42 -      SOME (h, _) => h
    2.43 -    | NONE => error ("Unexpected end of input" ^ Position.here pos))
    2.44 -  end;
    2.45 +fun read_header pos text =
    2.46 +  Symbol_Pos.explode (text, pos)
    2.47 +  |> Token.tokenize bootstrap_keywords {strict = false}
    2.48 +  |> read_tokens pos;
    2.49 +
    2.50 +val approx_length = 1024;
    2.51  
    2.52 -fun read pos str = read_source pos (token_source pos str);
    2.53 -fun read_tokens toks = read_source Position.none (Source.of_list toks);
    2.54 +in
    2.55 +
    2.56 +fun read pos text =
    2.57 +  if size text <= approx_length then read_header pos text
    2.58 +  else
    2.59 +    let val approx_text = String.substring (text, 0, approx_length) in
    2.60 +      if String.isSuffix "begin" approx_text then read_header pos text
    2.61 +      else (read_header pos approx_text handle ERROR _ => read_header pos text)
    2.62 +    end;
    2.63  
    2.64  end;
    2.65 +
    2.66 +end;