# Copyright 2010 Google Inc.
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#      http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# This is the main AppEngine content handler for serving Ghilbert.

import cgi
import urllib
import logging
import StringIO
import os

import verify
import babygit.web
import app.edit
import app.recent
import app.showthm
import app.users
import app.wiki
import app.workspace

import webapp2
from webapp2_extras import json

from google.appengine.api import users
from google.appengine.ext import db

# Return a stream over all proofs in the repository, including the base peano set.
# The proofs are ordered by number.  Optionally, you may provide one proof to be replaced.
# TODO: this probably doesn't have to all be in memory at once.
# TODO: this also shouldn't query the entire DB and sort.
def get_all_proofs(replacing=None, below=None):
    pipe = StringIO.StringIO()
    for line in open('peano/peano_thms.gh', 'r'):
        pipe.write(str(line))

    q = Proof.all()
    q.order('number')
    written = (replacing is None)
    for proof in q:
        if below is not None and proof.number >= below:
            break    
        if not written and proof.number > replacing.number:
            pipe.write(str(replacing.content))
            written = True
        if replacing is None or proof.name != replacing.name:
            pipe.write("# number %s\n" % str(proof.number))
            if proof.content is None:
                pipe.write("# proof.content is None\n")
            else:
                pipe.write(str(proof.content))
                pipe.write("\n")
    if not written:
        pipe.write(str(replacing.content))
    pipe.seek(0)
    return pipe

class Proof(db.Model):
    author = db.UserProperty()
    name = db.StringProperty()
    content = db.TextProperty()
    date = db.DateTimeProperty(auto_now=True)
    number = db.FloatProperty()
    
class Greeting(db.Model):
    author = db.UserProperty()
    content = db.StringProperty(multiline=True)
    date = db.DateTimeProperty(auto_now_add=True)

class RecentPage(webapp2.RequestHandler):
    def get(self):
        self.response.out.write("""<html><body>
<p>Recent saves:</p>""")

        proofs = db.GqlQuery("SELECT * FROM Proof ORDER BY date DESC LIMIT 10")

        for proof in proofs:
            if proof.author:
                self.response.out.write('<b>%s</b> wrote ' % proof.author.nickname())
            else:
                self.response.out.write('An anonymous person wrote ')
            self.response.out.write('<a href="/edit/%s">%s</a>:<br />' %
                                    (urllib.quote(proof.name),
                                     cgi.escape(proof.name)))
            if (proof.content is None):
                content = ""
            else:
                content = cgi.escape(proof.content)
            newcontent = []
            for line in content.rstrip().split('\n'):
                sline = line.lstrip()
                newcontent.append('&nbsp;' * (len(line) - len(sline)) + sline)
            content = '<br />'.join(newcontent)
            self.response.out.write('<blockquote>%s</blockquote>' % content)

class SaveHandler(webapp2.RequestHandler):
    def post(self):
        # Note, the following line gets the un-url-encoded name.
        name = self.request.get('name')
        proof = Proof.get_or_insert(name)
        proof.name = name
        proof.content = self.request.get('content')
        proof.number = float(self.request.get('number'))

        if users.get_current_user():
            proof.author = users.get_current_user()


        self.response.out.write("Verifying:\n")
        pipe = get_all_proofs(replacing=proof)
        url = '-'
        urlctx = verify.UrlCtx('','peano/peano_thms.gh', pipe)
        ctx = verify.VerifyCtx(urlctx, verify.run, False)
        ctx.run(urlctx, url, ctx, self.response.out)
        # Accept or reject
        if ctx.error_count > 0:
            self.response.out.write("\nCannot save; %d errors\n" % ctx.error_count)
        else:
            proof.put()
            self.response.out.write("\nsave ok\n")

class EditPage(webapp2.RequestHandler):
    def get(self, name):
        if name == '':
            name = 'new%20theorem'
        # name here is URL-encoded, we want to display the unencoded version
        # as text, and avoid the possibility of injection attack.
        name = urllib.unquote(name);
        q = Proof.all()