@@ -0,0 +1,2599 @@
+# Copyright 2012 Google Inc.%0A#%0A# Licensed under the Apache License, Version 2.0 (the %22License%22);%0A# you may not use this file except in compliance with the License.%0A# You may obtain a copy of the License at%0A#%0A#      http://www.apache.org/licenses/LICENSE-2.0%0A#%0A# Unless required by applicable law or agreed to in writing, software%0A# distributed under the License is distributed on an %22AS IS%22 BASIS,%0A# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.%0A# See the License for the specific language governing permissions and%0A# limitations under the License.%0A%0A# Utilities for processing text files, including patching and diffing,%0A# as well as semantic splitting of ghilbert proof files.%0A%0Adef count_char(line, ch, limit):%0A    count = 0%0A    i = 0%0A    while True:%0A        i = line.find(ch, i, limit)%0A        if i %3C 0: return count%0A        count += 1%0A        i += 1%0A%0Adef count_parens(line):%0A    limit = line.find('#')%0A    if limit == -1: limit = len(line)%0A    return count_char(line, '(', limit) - count_char(line, ')', limit)%0A%0Adef tokenize(line):%0A    line = line.split('#')%5B0%5D%0A    line = line.replace('(', ' ( ')%0A    line = line.replace(')', ' ) ')%0A    return line.split()%0A%0A# Returns a list of (name, startline, endline) tuples, where lines are%0A# 0-based, and exclusive of endline. Ignore comment blocks for now%0Adef split_gh_file(lines):%0A    level = 0%0A    result = %5B%5D%0A    startline = 0%0A    name = None%0A    for i, line in enumerate(lines):%0A        delta = count_parens(line)%0A        if level == 0 and name is None:%0A            if line.startswith('#!'):%0A                startline = i + 1%0A            elif startline == i and line.rstrip() == '':%0A                startline = i + 1%0A            else:%0A                toks = tokenize(line)%0A                if len(toks) %3E= 3 and toks%5B0%5D == 'thm' and toks%5B1%5D == '(':%0A                    name = toks%5B2%5D%0A                elif level + delta == 0 and len(toks) and toks%5B-1%5D == ')':%0A                    startline = i + 1%0A        level += delta%0A        if name is not None and level == 0:%0A            result.append((name, startline, i + 1))%0A            name = None%0A            startline = i + 1%0A    return result%0A%0A# for testing%0Aif __name__ == '__main__':%0A    import sys%0A    lines = file(sys.argv%5B1%5D).read().split('%5Cn')%0A    annot = split_gh_file(lines)%0A    print annot%0A    ix = 0%0A    pref = ''%0A    for i, line in enumerate(lines):%0A        if ix %3C len(annot) and i == annot%5Bix%5D%5B2%5D:%0A            pref = ''%0A            ix += 1%0A        if ix %3C len(annot) and i == annot%5Bix%5D%5B1%5D:%0A            pref = annot%5Bix%5D%5B0%5D + ':'%0A        print '%2510s %25s' %25 (pref, line)%0A%0A

Add utility function to split .gh file into thms