diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Source/ModelViewer/SourceView.cs | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Source/ModelViewer/SourceView.cs')
-rw-r--r-- | Source/ModelViewer/SourceView.cs | 104 |
1 files changed, 52 insertions, 52 deletions
diff --git a/Source/ModelViewer/SourceView.cs b/Source/ModelViewer/SourceView.cs index d520ede5..a40950b6 100644 --- a/Source/ModelViewer/SourceView.cs +++ b/Source/ModelViewer/SourceView.cs @@ -1,52 +1,52 @@ -using System;
-using System.Collections.Generic;
-using System.ComponentModel;
-using System.Data;
-using System.Drawing;
-using System.Linq;
-using System.Text;
-using System.Windows.Forms;
-
-namespace Microsoft.Boogie.ModelViewer
-{
- public partial class SourceView : Form
- {
- public bool largeFont;
- bool prevLarge;
-
- public SourceView()
- {
- InitializeComponent();
- //richTextBox1.Font = new Font(richTextBox1.Font.FontFamily, fontSize, richTextBox1.Font.Unit);
- richTextBox1.BackColor = Color.White;
- }
-
- string prevRtf;
-
- string prefix =
- @"{\rtf1\ansi\ansicpg1252\deff0\deflang1033{\fonttbl{\f0\fnil\fcharset0 Lucida Sans Typewriter;}}\r\n" +
- @"{\colortbl;\red0\green0\blue0;\red255\green0\blue0;\red0\green255\blue0;\red255\green255\blue0;\red0\green0\blue0;\red160\green160\blue160;}" +
- @"\viewkind4\uc1\pard\f0";
-
- internal void SetSourceLocation(SourceViewState r)
- {
- if (r.RichTextContent != prevRtf || prevLarge != largeFont) {
- richTextBox1.Rtf = prefix + (largeFont ? "\\fs30 " : "\\fs17 ") + r.RichTextContent + "\r\n}\r\n";
- prevRtf = r.RichTextContent;
- prevLarge = largeFont;
- }
-
- richTextBox1.Select(r.Location, 9);
-
- this.Text = r.Header;
- this.Show();
- }
-
- protected override void OnClosing(CancelEventArgs e)
- {
- base.OnClosing(e);
- e.Cancel = true;
- Hide();
- }
- }
-}
+using System; +using System.Collections.Generic; +using System.ComponentModel; +using System.Data; +using System.Drawing; +using System.Linq; +using System.Text; +using System.Windows.Forms; + +namespace Microsoft.Boogie.ModelViewer +{ + public partial class SourceView : Form + { + public bool largeFont; + bool prevLarge; + + public SourceView() + { + InitializeComponent(); + //richTextBox1.Font = new Font(richTextBox1.Font.FontFamily, fontSize, richTextBox1.Font.Unit); + richTextBox1.BackColor = Color.White; + } + + string prevRtf; + + string prefix = + @"{\rtf1\ansi\ansicpg1252\deff0\deflang1033{\fonttbl{\f0\fnil\fcharset0 Lucida Sans Typewriter;}}\r\n" + + @"{\colortbl;\red0\green0\blue0;\red255\green0\blue0;\red0\green255\blue0;\red255\green255\blue0;\red0\green0\blue0;\red160\green160\blue160;}" + + @"\viewkind4\uc1\pard\f0"; + + internal void SetSourceLocation(SourceViewState r) + { + if (r.RichTextContent != prevRtf || prevLarge != largeFont) { + richTextBox1.Rtf = prefix + (largeFont ? "\\fs30 " : "\\fs17 ") + r.RichTextContent + "\r\n}\r\n"; + prevRtf = r.RichTextContent; + prevLarge = largeFont; + } + + richTextBox1.Select(r.Location, 9); + + this.Text = r.Header; + this.Show(); + } + + protected override void OnClosing(CancelEventArgs e) + { + base.OnClosing(e); + e.Cancel = true; + Hide(); + } + } +} |